proposition: Lemma pair_mOrd_fromList : aL >=A aR -> bL >=A bR -> aL >A aR \/ bL >A bR -> list2multiset (aL :: bL :: nil) >MUL list2multiset (aR :: bR :: nil).
proof: Proof. intros. setoid_replace (list2multiset (aL :: bL :: nil)) with {{aL, bL}}. setoid_replace (list2multiset (aR :: bR :: nil)) with {{aR, bR}}. destruct H1. apply pair_mOrd_left; trivial. apply pair_mOrd_right; trivial. simpl. solve_meq. simpl. solve_meq. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)