proposition: Lemma card_non_empty M : M <>mul empty -> card M > 0.
proof: Proof. intros. unfold card; destruct (card_def M); simpl. assert (w := multiset2list_meq_non_empty H). destruct (multiset2list M); try_solve. rewrite <- e; auto with arith. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)