proposition: Lemma pair_mOrd : {{ aL, bL }} >MUL {{ aR, bR }} -> (aL >=A aR /\ aL >=A bR /\ (aL >A aR \/ aL >A bR)) \/ (bL >=A aR /\ bL >=A bR /\ (bL >A aR \/ bL >A bR)) \/ (aL >=A aR /\ bL >=A bR /\ (aL >A aR \/ bL >A bR)) \/ (bL >=A aR /\ aL >=A bR /\ (bL >A aR \/ aL >A bR)).
proof: Proof. intros. inversion H. destruct (pair_decomp H1) as [[ZaLbL Xempty] | [[Zempty XaLbL] | [[ZaL XbL] | [ZbL XaL]]]]. absurd (X =mul= empty); trivial. assert (Y =mul= {{aR, bR}}). rewrite H2, Zempty; solve_meq. destruct (H3 aR). rewrite H4; mset_unfold. apply member_union_l; auto with multisets. assert (x in {{aL, bL}}). rewrite <- XaLbL; trivial. destruct (H3 bR). rewrite H4; mset_unfold. apply member_union_r; auto with multisets. assert (x0 in {{aL, bL}}). rewrite <- XaLbL; trivial. destruct (member_pair H7); destruct (member_pair H10). left; repeat split; rewrite <- H11; try solve [left; trivial]. left; rewrite H11, <- H12; trivial. right; right; left; repeat split; try rewrite <- H11; try rewrite <- H12; try solve [left; trivial]. right; right; right; repeat split; try rewrite <- H11; try rewrite <- H12; try solve [left; trivial]. right; left; repeat split; rewrite <- H11; try solve [left; trivial]. left; rewrite H11, <- H12; trivial. destruct (eqA_dec aL aR). assert (Y =mul= {{bR}}). setoid_replace Y with (Z + Y - Z). rewrite <- (meq_diff_meq Z H2), ZaL, e. solve_meq. solve_meq. destruct (H3 bR). rewrite H4; auto with multisets. assert (bL >A bR). setoid_replace bL with x; trivial. apply Seq_sym. exact eqA_Equivalence. apply member_singleton. rewrite <- XbL; trivial. right; right; left; repeat split. right; trivial. left; trivial. right; trivial. destruct (eqA_dec aL bR). assert (Y =mul= {{aR}}). setoid_replace Y with (Z + Y - Z). rewrite <- (meq_diff_meq Z H2), ZaL, e. solve_meq. solve_meq. destruct (H3 aR). rewrite H4; auto with multisets. assert (bL >A aR). setoid_replace bL with x; trivial. apply Seq_sym. exact eqA_Equivalence. apply member_singleton. rewrite <- XbL; trivial. right; right; right; repeat split. left; trivial. right; trivial. left; trivial. absurd (mult aL {{aR, bR}} = mult aL (Z + Y)). mset_unfold; rewrite !union_mult, !singleton_mult_notin; trivial. assert (aL in Z). rewrite ZaL; auto with multisets. unfold member in H4; lia. apply meq_multeq; trivial. destruct (eqA_dec bL aR). assert (Y =mul= {{bR}}). setoid_replace Y with (Z + Y - Z). rewrite <- (meq_diff_meq Z H2), ZbL, e. solve_meq. solve_meq. destruct (H3 bR). rewrite H4; auto with multisets. assert (aL >A bR). setoid_replace aL with x; trivial. apply Seq_sym. exact eqA_Equivalence. apply member_singleton. rewrite <- XaL; trivial. right; right; right; repeat split. right; trivial. left; trivial. right; trivial. destruct (eqA_dec bL bR). assert (Y =mul= {{aR}}). setoid_replace Y with (Z + Y - Z). rewrite <- (meq_diff_meq Z H2), ZbL, e. solve_meq. solve_meq. destruct (H3 aR). rewrite H4; auto with multisets. assert (aL >A aR). setoid_replace aL with x; trivial. apply Seq_sym. exact eqA_Equivalence. apply member_singleton. rewrite <- XaL; trivial. right; right; left; repeat split. left; trivial. right; trivial. left; trivial. absurd (mult bL {{aR, bR}} = mult bL (Z + Y)). mset_unfold; rewrite !union_mult, !singleton_mult_notin; trivial. assert (bL in Z). rewrite ZbL; auto with multisets. unfold member in H4; lia. apply meq_multeq; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)