proposition: Lemma union_card M N : card (M + N) = (card M + card N)%nat.
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_union_length. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)