proposition: Lemma pair_mOrd_left : aL >A aR -> bL >=A bR -> {{ aL, bL }} >MUL {{ aR, bR }}.
proof: Proof. intros. destruct H0. constructor 1 with {{aL, bL}} {{aR, bR}} empty; try solve_meq. intros. destruct (member_pair H1). exists aL. unfold pair; apply member_insert. rewrite H2; trivial. exists bL. unfold pair, insert; auto with multisets. rewrite H2; trivial. constructor 1 with {{aL}} {{aR}} {{bL}}; try solve_meq. rewrite H0; solve_meq. intros. exists aL. auto with multisets. rewrite (member_singleton H1); trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)