proposition: Lemma insert_diff a M N : insert a M - N =mul= empty -> a in N /\ M - remove a N =mul= empty.
proof: Proof. intros. assert (a in N). destruct (member_dec a N); trivial. exfalso. apply not_empty with empty a; auto with multisets. fold (member a empty). rewrite <- H. apply diff_member_ly_rn; eauto with multisets. apply member_insert. split; trivial. rewrite <- H. rewrite (diff_remove_both (member_insert a M) H0). solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)