proposition: Lemma union_notempty M N : M <>mul empty -> M + N <>mul empty.
proof: Proof. compute in *; intros; apply H. apply union_isempty with N; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)