proposition: Lemma ltM_inv3: forall l l' a b n b' n', a < b' -> nf (cons b n l) -> nf (cons b' n' l') -> ltM a (cons b n l) (cons b' n' l') -> b = b' /\ n = n'.
proof: Proof. intros. case H2. intros. case (trichotomy_inf b b'). destruct 1. generalize (H4 _ H). rewrite nf_multiplicity_big;auto. rewrite nf_multiplicity_head. discriminate 1. auto. split. auto. subst b'. generalize (H4 _ H). rewrite nf_multiplicity_head ;auto. rewrite nf_multiplicity_head ;auto. intro. assert (lt a b). eapply lt_trans;eauto. generalize (H4 _ H5). rewrite nf_multiplicity_head ;auto. rewrite nf_multiplicity_big ;auto. intro;absurd (0<n)%nat. discriminate H6. discriminate H6. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0