proposition: Lemma red_insert: forall M N a, N <mul_1 (M + {{a}}) -> exists M', (N =mul= M' + {{a}} /\ M' <mul_1 M) \/ (N =mul= M + M' /\ forall x, x in M' -> x <A a).
proof: Proof. intros; inversion H. case (eqA_dec a a0); intro a_a0. exists Y; right; split. rewrite H1; setoid_replace X with M. auto with multisets. apply meq_union_meq with {{a}}. rewrite <- a_a0 in H0. auto with multisets. intros; rewrite a_a0; apply (H2 x); trivial. assert (a0_a: ~a0 =A= a); auto with sets. exists (Y + (M - {{a0}})); left; split. rewrite H1; setoid_replace X with (M - {{a0}} + {{a}}). 2: rewrite (meq_ins_ins (meq_sym H0)); auto with multisets. 2: try_solve_meq; case (eqA_dec x a); case (eqA_dec x a0); intros; try_solve_meq_ext. try_solve_meq. constructor 1 with (M - {{a0}}) a0 Y; auto with multisets. apply meq_ins_rem; eauto with multisets. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)