proposition: Lemma pair_decomp a b X Y : {{a, b}} =mul= X + Y -> (X =mul= {{a, b}} /\ Y =mul= empty) \/ (X =mul= empty /\ Y =mul= {{a, b}}) \/ (X =mul= {{a}} /\ Y =mul= {{b}}) \/ (X =mul= {{b}} /\ Y =mul= {{a}}).
proof: Proof. intros. destruct (empty_decomp_dec X) as [[[X1 c] X1c] | Xempty]. simpl in X1c. destruct (empty_decomp_dec X1) as [[[X2 d] X2d] | X1empty]. simpl in X2d. destruct (empty_decomp_dec X2) as [[[X3 e] X3e] | X2empty]. simpl in X3e. absurd (card {{a, b}} = card (X + Y)). repeat (rewrite union_card; try rewrite (card_morph X1c); try rewrite (card_morph X2d); try rewrite (card_morph X3e)). rewrite pair_card, !singleton_card; lia. apply (card_morph H). assert (Y =mul= empty). destruct (empty_decomp_dec Y) as [[[Y1 e] Y1e] | Yempty]; trivial. simpl in Y1e. absurd (card {{a, b}} = card (X + Y)). repeat (rewrite union_card; try rewrite (card_morph X1c); try rewrite (card_morph X2d); try rewrite (card_morph Y1e)). rewrite pair_card, !singleton_card; lia. apply (card_morph H). left; split; trivial. rewrite H, X1c, X2d, X2empty, H0; solve_meq. destruct (empty_decomp_dec Y) as [[[Y1 d] Y1d] | Yempty]; trivial. simpl in Y1d. destruct (empty_decomp_dec Y1) as [[[Y2 e] Y2e] | Y1empty]; trivial. simpl in Y2e. absurd (card {{a, b}} = card (X + Y)). repeat (rewrite union_card; try rewrite (card_morph X1c); try rewrite (card_morph Y1d); try rewrite (card_morph Y2e)). rewrite pair_card, !singleton_card; lia. apply (card_morph H). destruct (@pair_eq a b c d) as [[ac bd] | [ad bc]]. rewrite H, X1c, Y1d, X1empty, Y1empty; solve_meq. right; right; left; split. rewrite X1c, X1empty, ac; solve_meq. rewrite Y1d, Y1empty, bd; solve_meq. right; right; right; split. rewrite X1c, X1empty, bc; solve_meq. rewrite Y1d, Y1empty, ad; solve_meq. absurd (card {{a, b}} = card (X + Y)). repeat (rewrite union_card; try rewrite (card_morph X1c); try rewrite (card_morph X1empty); try rewrite (card_morph Yempty)). rewrite pair_card, !singleton_card; lia. apply (card_morph H). destruct (empty_decomp_dec Y) as [[[Y1 c] Y1c] | Yempty]; trivial. simpl in Y1c. destruct (empty_decomp_dec Y1) as [[[Y2 d] Y2d] | Y1empty]; trivial. simpl in Y2d. destruct (empty_decomp_dec Y2) as [[[Y3 e] Y3e] | Y2empty]; trivial. simpl in Y3e. absurd (card {{a, b}} = card (X + Y)). repeat (rewrite union_card; try rewrite (card_morph Y1c); try rewrite (card_morph Y2d); try rewrite (card_morph Y3e)). rewrite pair_card, !singleton_card; lia. apply (card_morph H). right; left; split; trivial. rewrite H, Y1c, Y2d, Y2empty, Xempty; solve_meq. absurd (card {{a, b}} = card (X + Y)). repeat (rewrite union_card; try rewrite (card_morph Xempty); try rewrite (card_morph Y1c); try rewrite (card_morph Y1empty)). rewrite pair_card, !singleton_card; lia. apply (card_morph H). absurd (card {{a, b}} = card (X + Y)). repeat (rewrite union_card; try rewrite (card_morph Xempty); try rewrite (card_morph Yempty)). rewrite pair_card; rewrite empty_card; lia. apply (card_morph H). Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)