proposition: Lemma singleton_mult_union_empty a a' M : {{a}} =mul= {{a'}} + M -> M =mul= empty.
proof: Proof. intros. destruct M using mset_ind; auto with multisets. assert ({{a}} =mul= {{a'}} + {{a0}} + M). rewrite H; solve_meq. clear H IHM. destruct (eqA_dec a a'). destruct (eqA_dec a a0). absurd (a/{{a}} = a/({{a'}} + {{a0}} + M)). rewrite !union_mult, !singleton_mult_in; auto with sets. lia. apply meq_multeq; trivial. absurd ((a0/({{a'}} + {{a0}} + M))%msets > 0). rewrite <- (meq_multeq H0 a0). rewrite singleton_mult_notin; auto with sets arith. rewrite !union_mult, singleton_mult_in with a0 a0; auto with sets arith. absurd ((a'/({{a'}} + {{a0}} + M))%msets > 0). rewrite <- (meq_multeq H0 a'). rewrite singleton_mult_notin; auto with sets arith. rewrite !union_mult, singleton_mult_in with a' a'; auto with sets arith. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)