proposition: Lemma transitivity0 : forall n, forall t1 t2 t3, (length t1 + length 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. inversion 1. inversion 1. inversion 2. auto with T2. inversion 3. auto with T2. inversion 2. inversion 3. 2:inversion 3. inversion H0. intros. eapply trans_aux. eexact H0. auto with T2. intros. apply IHn with t'. omega. auto with T2. auto with T2. Qed.
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