proposition: Lemma pair_mord_left : aL >A aR -> bL >=A bR -> {{ aL, bL }} >mul {{ aR, bR }}.
proof: Proof. intros; destruct H0. constructor 2 with {{aR, bL}}. constructor; constructor 1 with {{bL}} aL {{aR}}; intros; eauto with multisets. assert (xAr: y =A= aR); [apply member_singleton | rewrite xAr]; trivial. constructor; constructor 1 with {{aR}} bL {{bR}}; intros; eauto with multisets. assert (xAr: y =A= bR); [apply member_singleton | rewrite xAr]; trivial. rewrite H0. constructor; constructor 1 with {{bR}} aL {{aR}}; intros; eauto with multisets. assert (xAr: y =A= aR); [apply member_singleton | rewrite xAr]; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)