proposition: Lemma mOrd_elts_ge : M >MUL N -> (forall n, n in N -> exists2 m, m in M & m >=A n).
proof: Proof. intros. destruct H as [X Y Z Xne MZX NZY Cond]. assert (nn: n =A= n); auto with sets. set (nZY := proj1 (member_morph nn NZY) H0). destruct (member_union nZY). exists n. rewrite MZX. apply member_member_union; trivial. right; trivial. destruct (Cond n H) as [m mX mn]. exists m. rewrite MZX, (union_comm Z X). apply member_member_union; trivial. left; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)