proposition: Lemma multiset2list_cons_length M a : length (multiset2list (M + {{a}})) = S (length (multiset2list M)).
proof: Proof. intros; unfold multiset2list. destruct (mult_to_list (M + {{a}})). destruct (mult_to_list M); simpl. apply list2multiset_cons_length with a. rewrite <- m0; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)