proposition: Lemma tricho_aux : forall l, forall t t', (length t + length t' < l)%nat -> { t < t'}+{t = t'}+{t'< t}.
proof: Proof. induction l. intros. elimtype False. inversion H. intros t t'. case t;case t'. left;right;auto with T2. left;left;constructor. right;constructor. intros. assert (length t3 + length t0 < l)%nat. eapply lt_lt_Sn. eapply tricho_lt_2. eauto with T2. case (IHl _ _ H0). destruct 1. assert (length t4 + length (cons t0 t1 0 zero) < l)%nat. eapply lt_lt_Sn. eapply tricho_lt_2'. eauto. case (IHl _ _ H1). destruct 1. left;left. constructor 2;auto with T2. subst t4. right. constructor 5;auto with T2. intro. right. constructor 4;auto with T2. subst t3. assert (length t4 + length t1 < l)%nat. eapply lt_lt_Sn. eapply tricho_lt_3. eauto with T2. case (IHl _ _ H1). destruct 1. left;left. constructor 3. auto with T2. subst t4. case (lt_eq_lt_dec n0 n). destruct 1. left;left. constructor 6. auto with T2. subst n. assert (length t5 + length t2 < l)%nat. eapply lt_lt_Sn. eapply tricho_lt_7. eauto with T2. case (IHl _ _ H2). destruct 1. left;left. constructor 7;auto with T2. subst t2. left;right;trivial. intro. right;constructor 7;auto with T2. right. constructor 6;auto with T2. intro. right;constructor 3;auto with T2. intro. assert (length t1 + length (cons t3 t4 0 zero) < l)%nat. eapply lt_lt_Sn. eapply tricho_lt_2'. rewrite plus_comm. eauto with T2. case (IHl _ _ H1). destruct 1. right. constructor 2;auto with T2. subst t1. left;left;constructor 5;auto with T2. left;left;constructor 4;auto with T2. Defined.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo