proposition: Lemma member_notempty M x : x in M -> M <>mul empty.
proof: Proof. unfold not; intros. absurd (mult x M = 0). unfold member in H; lia. rewrite (meq_multeq H0); auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)