proposition: Lemma not_empty M x : x in M -> M =mul= empty -> False.
proof: Proof. unfold member; intros mult_x_M M_is_empty. absurd (x/M = 0). lia. assert (x/empty = 0); [auto with multisets | idtac]. assert (x/M = x/empty); [apply meq_multeq; trivial | idtac]. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)