proposition: Lemma tricho_aux (l: nat) : forall t t': T2, t2_length t + t2_length t' < l -> {t t2< t'} + {t = t'} + {t' t2< t}.
proof: Proof. induction l. - intros; assert False by inversion H; contradiction. - intros t t'; case t;case t'. + left;right;auto with T2. + left;left;constructor. + right;constructor. + intros t0 t1 n t2 t3 t4 n0 t5 H. assert (H0 :(t2_length t3 + t2_length t0 < l)%nat). { eapply lt_lt_Sn. eapply tricho_lt_2. eauto with T2. } case (IHl _ _ H0). * destruct 1. assert (t2_length t4 + t2_length (gcons 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 H2; right; constructor 4;auto with T2. -- subst t3; assert (H1: (t2_length t4 + t2_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 (Compare_dec.lt_eq_lt_dec n0 n). destruct 1. { left;left; constructor 6. auto with T2. } subst n; assert (H2:(t2_length t5 + t2_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 H3; right;constructor 7;auto with T2. right; constructor 6;auto with T2. ++ intro H2; right;constructor 3;auto with T2. * intro H1; assert (H2:(t2_length t1 + t2_length (gcons t3 t4 0 zero) < l)%nat). -- eapply lt_lt_Sn. ++ eapply tricho_lt_2'. ++ rewrite Nat.add_comm; eauto with T2. -- case (IHl _ _ H2). ++ 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: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)