proposition: Lemma pred_LT : forall alpha beta, nf alpha -> pred alpha = Some beta -> beta t1< alpha .
proof: Proof. intros; destruct (zero_limit_succ_dec H). - destruct s. + subst; discriminate. + rewrite pred_of_limit in H0; trivial. * discriminate. - destruct s. destruct a. subst; rewrite pred_of_succ in H0; trivial. + injection H0; intros; subst x; split; auto. split; auto. now apply lt_succ. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)