proposition: Lemma ltM_lt : forall a l l', nf l -> nf l' -> ltM a l l' -> l < l'.
proof: Proof. induction l; destruct l'. intros; absurd (ltM a zero zero);auto. unfold ltM;simpl. red; case (1). destruct 2. inversion H2. simpl. auto with T1. inversion 3. inversion H2. intros. case (trichotomy_inf l1 l'1). destruct 1. constructor 2;auto. subst l'1. case (trichotomy_inf a l1). destruct 1. case H1;intros. rewrite (nf_multiplicity_tail _ _ _ _ l H) in H2. rewrite (nf_multiplicity_tail _ _ _ _ l H0) in H2. generalize (H3 _ l). rewrite nf_multiplicity_head . rewrite nf_multiplicity_head . injection 1. intro; subst n0. constructor 4. apply IHl2. inversion_clear H; eauto. constructor. inversion_clear H0; eauto. constructor. split. auto. intros b H11. generalize (H3 _ H11). simpl. case (T1_eq_dec b l1). intros; clear H3; omega. auto. auto. auto. subst l1. case H1;intros. do 2 rewrite nf_multiplicity_head in H2. constructor 3;auto. clear H3;omega. auto. auto. auto. case H1;intros. do 2 rewrite nf_multiplicity_big in H2. inversion_clear H2. auto. auto. auto. auto. auto. auto. auto. auto. intro. generalize (ltM_inv2 _ _ _ _ _ _ _ H H0 H1). destruct 1. subst l'1. case H1;intros. generalize (H3 _ l). rewrite (nf_multiplicity_head);auto. rewrite (nf_multiplicity_big);auto. intro. discriminate H4. generalize (ltM_inv3 _ _ _ _ _ _ _ H2 H H0 H1). destruct 1. subst l'1. case (lt_irr l). Qed.
imports: Arith Omega ArithRing More_nat EPSILON0