proposition: Lemma lt_trans0 : forall n, forall t1 t2 t3, (t2_length t1 + t2_length t2 + t2_length t3 < n)%nat -> lt t1 t2 -> lt t2 t3 -> lt t1 t3.
proof: Proof. induction n. - inversion 1. - destruct t1; destruct t2; destruct t3. + intros; trivial. + inversion 2. + inversion 3. + auto with T2. + inversion 2. + inversion 3. inversion H0. + inversion 3. + intros; eapply trans_aux. * eexact H0. * auto with T2. * intros; apply IHn with t'; auto with T2. -- lia. Qed.
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)