proposition: Lemma ltM_inv : forall a b n l l', nf (cons b n l) -> nf (cons b n l') -> ltM a (cons b n l) (cons b n l') -> ltM a l l'.
proof: Proof. inversion_clear 3. case (trichotomy_inf a b). destruct 1. do 2 rewrite nf_multiplicity_tail in H2; auto. split;auto. intros. generalize (H3 _ H1). simpl. case (T1_eq_dec b0 b). auto. clear H3;intro;omega. auto. subst b; do 2 rewrite nf_multiplicity_head in H2;auto. absurd (n<n)%nat; auto with arith. intro. do 2 rewrite nf_multiplicity_big in H2;auto. inversion H2. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0