proposition: Lemma member_ins_ins_meq a a' M M' : M + {{a}} =mul= M' + {{a'}} -> ~a =A= a' -> a in M'.
proof: Proof. intros. assert (((a/M)%msets + 1)%nat = ((a/M')%msets + 0)%nat). rewrite <- (singleton_mult_in ((Seq_refl A eqA eqA_Equivalence) a)), <- (singleton_mult_notin H0), <- !union_mult. apply meq_multeq; trivial. mset_unfold; lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)