proposition: Lemma LT_of_finite : forall alpha n, alpha t1< FS n -> alpha = zero \/ exists p, p < n /\ alpha = FS p.
proof: Proof. intros alpha n [H1 [H2 H3]]. destruct alpha. - now left. - T1_inversion H2. T1_inversion H. destruct H as [[H4 H5] |[H4 [H5 H6]]]. subst. generalize (nf_of_finite H1). intro;subst. right; exists n0. split; auto with T1 arith. T1_inversion H6. 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)