proposition: Lemma list2multiset_cons_length l l' : forall a, list2multiset l + {{a}} =mul= list2multiset l' -> length l' = S (length l).
proof: Proof. destruct l'. simpl; intros. exfalso. apply not_empty with (list2multiset l + {{a}}) a; trivial. apply member_union_r; auto with multisets. intros. change (S (length l)) with (length (a0 :: l)). apply permutation_length with eqA eqA_dec. exact eqA_Equivalence. apply meq_permutation. rewrite <- H. simpl; solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)