proposition: Theorem transitivity : forall t1 t2 t3, t1 < t2 -> t2 < t3 -> t1 < t3.
proof: Proof. intros; apply transitivity0 with (S (length t1 + length t2 + length t3)) t2; auto with T2 arith. 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