proposition: Lemma mord_elts_ge: M >mul N -> forall n, n in N -> exists2 m, m in M & m >*A n \/ m =A= n.
proof: Proof. induction 1 as [M N M_N | M N P M_N IH_MN N_P IH_NP]; intros n n_in_N. destruct M_N as [X a Y Mdef Ndef Ya_ord]. cut (n in N); [rewrite Ndef | trivial]. intros n_in_XY; destruct (member_union n_in_XY) as [n_in_X | n_in_Y]. exists n. rewrite Mdef; auto with multisets. right; auto with sets. exists a. rewrite Mdef; auto with multisets. left; constructor; auto with sets. destruct (IH_NP n n_in_N) as [np np_in_N np_ge_n]. destruct (IH_MN np np_in_N) as [mp mp_in_M mp_ge_n]. exists mp. trivial. destruct np_ge_n as [np_gt_n | np_n]. destruct mp_ge_n as [mp_gt_n | mp_n]. left; constructor 2 with np; trivial. left; rewrite mp_n; trivial. rewrite <- np_n; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)