proposition: Lemma lt_ltM2 : forall c c', nf c -> nf c' -> c < c' -> {a:T1| ltM a c c'}.
proof: Proof. induction c; destruct c'. intros; elimtype False. inversion H1. exists c'1;simpl. constructor. simpl. case (T1_eq_dec c'1 c'1). auto with arith. intros; absurd (c'1=c'1);auto. intros;rewrite nf_multiplicity_big. simpl;auto. auto. auto. intros;elimtype False. inversion H1. intros. case (trichotomy_inf c1 c'1). destruct 1. exists c'1. simpl. inversion H1. split. rewrite nf_multiplicity_big. rewrite nf_multiplicity_head. auto with arith. auto. auto. auto. intros; repeat rewrite nf_multiplicity_big. auto. auto. auto. eapply lt_trans;eauto. auto. split. repeat rewrite nf_multiplicity_head. auto with arith. auto. subst c'1. auto. intros. repeat rewrite nf_multiplicity_big;auto. subst c'1;auto. subst c'1; case (lt_irr l). subst c'1. case (lt_eq_lt_dec n n0). destruct 1. exists c1. split. repeat rewrite nf_multiplicity_head. auto with arith. auto. auto. intros; repeat rewrite nf_multiplicity_big;auto. subst n0. assert (lt c2 c'2). eapply lt_inv_b;eauto. case (IHc2 c'2). eapply nf_inv2;eauto. eapply nf_inv2;eauto. auto. intros;exists x. apply ltM_cons. auto. intros. elimtype False. generalize (lt_inv_nb H1). destruct 1. absurd (n<n)%nat;eauto with arith. case H2;intros ;subst n. absurd (n0<n0)%nat;auto with arith. intros. absurd (EPSILON0.le c1 c'1). unfold EPSILON0.le. red; destruct 1. subst c'1;case (lt_irr l). case (lt_not_gt l);auto. inversion H1. right;auto. subst c1;left;auto. left. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0