proposition: Lemma cons_eq_cons_cons_absurd a a' a'' M : {{a}} =mul= {{a'}} + {{a''}} + M -> False.
proof: Proof. intro. absurd ({{a}} =mul= insert a' (insert a'' M)); trivial. assert (M + {{a'}} + {{a''}} =mul= {{a}}). rewrite H; solve_meq. destruct (meq_cons H0) as [m' [am'a1 xa0m']]. absurd (m' =mul= empty). intro mempty. apply not_empty with m' a'; trivial. unfold member; rewrite <- (meq_multeq xa0m' a'). fold (member a' (M + {{a'}})). apply member_union_r; auto with multisets. apply (@singleton_mult_union_empty a a'' m'). rewrite am'a1; auto with multisets. rewrite H; solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)