proposition: Lemma diff_card M N : card (M - N) >= card M - card N.
proof: Proof. unfold card. destruct (card_def (M - N)); destruct (card_def M); destruct (card_def N); simpl. rewrite <- e; rewrite <- e0; rewrite <- e1. apply multiset2list_diff_length. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)