proposition: Lemma notempty_member M : M <>mul empty -> exists N a, M =mul= {{a}} + N.
proof: Proof. intros H. destruct M using mset_ind. absurd (empty =mul= empty); auto with multisets. ex M a. apply union_comm. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)