proposition: Lemma mord_ext1: forall M N a, M >mul N <-> M + {{a}} >mul N + {{a}}.
proof: Proof. intros; split; intros. destruct (proj1 (red_eq_direct M N) H). rewrite_rl (red_eq_direct (M + {{a}}) (N + {{a}})). constructor 1 with X Y (insert a Z); solve [solve_meq_ext; auto]. destruct (proj1 (red_eq_direct (M + {{a}}) (N + {{a}})) H). rewrite_rl (red_eq_direct M N). case (member_dec a Z); intro a_Z. constructor 1 with X Y (Z - {{a}}); solve [ apply ins_meq_union; trivial | auto]. assert (a_in_X: a in X). apply member_meq_union with {{a}} M Z; auto with multisets. rewrite (union_comm {{a}} M), (union_comm X Z); auto with multisets. assert (a_in_Y: a in Y). apply member_meq_union with {{a}} N Z; auto with multisets. rewrite (union_comm {{a}} N), (union_comm Y Z); auto with multisets. constructor 1 with (X - {{a}}) (Y - {{a}}) Z. destruct (H3 a); [trivial | idtac]. apply member_notempty with x. apply mem_memrem; eauto with sets. rewrite (union_comm Z (X - {{a}})); eauto with multisets. rewrite (union_comm Z (Y - {{a}})); eauto with multisets. apply mord_ext1_aux; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)