proposition: Lemma succ_lt_le : forall a b, nf a -> nf b -> a t2< succ b -> a t2<= b.
proof: Proof. intros. tricho a b H2; auto with T2. - generalize (lt_succ_le H2 H); intro; case (lt_irr (alpha:=succ b)). eapply le_lt_trans;eauto with T2. 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)