proposition: Lemma mord_wf_1: forall a M0, (forall b M, b <A a -> AccM_1 M -> AccM_1 (M + {{b}})) -> AccM_1 M0 -> (forall M, M <mul_1 M0 -> AccM_1 (M + {{a}})) -> AccM_1 (M0 + {{a}}).
proof: Proof. intros a M0 H1 H2 H3; constructor; intros N N_lt. case (red_insert N_lt); intros; repeat destruct H; fold AccM_1; rewrite H. apply H3; trivial. clear H N_lt H3; induction x as [|M a0] using mset_ind. setoid_replace (M0 + empty) with M0; auto with multisets. setoid_replace (M0 + (M + {{a0}})) with ((M0 + M) + {{a0}}). auto with multisets. auto with multisets. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)