proposition: Lemma ltM_inv2 : forall l l' a b n b' n', nf (cons b n l) -> nf (cons b' n' l') -> ltM a (cons b n l) (cons b' n' l') -> a <= b'.
proof: Proof. intros. case H1. intros H2 H3. case (trichotomy_inf a b'). destruct 1. auto. auto. right;auto. left;auto. intro. rewrite (nf_multiplicity_big _ _ _ _ l0 H0) in H2;auto. inversion H2. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0