proposition: Lemma multiset2list_diff_length M N : length (multiset2list (M - N)) >= length (multiset2list M) - length (multiset2list N).
proof: Proof. intros; unfold multiset2list. destruct (mult_to_list (M - N)); destruct (mult_to_list M); destruct (mult_to_list N); simpl. apply list2multiset_diff_length. rewrite <- m; rewrite <- m0; rewrite <- m1; auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)