proposition: Lemma pair_eq a b c d : {{a, b}} =mul= {{c, d}} -> (a =A= c /\ b =A= d) \/ (a =A= d /\ b =A= c).
proof: Proof. intros. destruct (eqA_dec a c). destruct (eqA_dec b d). left; split; trivial. destruct (eqA_dec a d). absurd (mult b {{a, b}} = mult b {{c, d}}). unfold pair, insert. rewrite !union_mult. rewrite (@singleton_mult_in b b); auto with sets. rewrite (@singleton_mult_notin b a); eauto with sets. rewrite (@singleton_mult_notin b c); eauto with sets. rewrite (@singleton_mult_notin b d); [|eauto with sets]. lia. setoid_replace c with d; eauto with sets. apply meq_multeq; trivial. absurd (mult d {{a, b}} = mult d {{c, d}}). unfold pair, insert. rewrite !union_mult. rewrite (@singleton_mult_notin d a); auto with sets. rewrite (@singleton_mult_notin d b); auto with sets. rewrite (@singleton_mult_in d d); auto with sets. lia. apply meq_multeq; trivial. destruct (eqA_dec a d). destruct (eqA_dec b c). right; split; trivial. absurd (mult c {{a, b}} = mult c {{c, d}}). unfold pair, insert. rewrite !union_mult. rewrite (@singleton_mult_notin c a); auto with sets. rewrite (@singleton_mult_notin c b); auto with sets. rewrite (@singleton_mult_in c c); auto with sets. apply meq_multeq; trivial. absurd (mult a {{a, b}} = mult a {{c, d}}). unfold pair, insert. rewrite !union_mult. rewrite (@singleton_mult_notin a c); auto with sets. rewrite (@singleton_mult_notin a d); auto with sets. rewrite (@singleton_mult_in a a); auto with sets. apply meq_multeq; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)