proposition: Lemma meq_cons a M N : M + {{a}} =mul= N -> exists N', N =mul= N' + {{a}} /\ M =mul= N'.
proof: Proof. intros. exists (remove a N); split. assert (aN: a in N). rewrite <- H. rewrite (union_comm M {{a}}). fold (insert a M); apply member_insert. set (N' := N) in |- * at 1. rewrite (meq_ins_rem aN); unfold N'; clear N'. rewrite (meq_remove_insert a (N - {{a}})). apply meq_ins_rem; trivial. rewrite <- H. solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)