proposition: Lemma T1is_succ_iff alpha (Halpha : nf alpha) : T1is_succ alpha <-> exists beta : T1, nf beta /\ alpha = succ beta.
proof: Proof. split. - intro H; destruct (T1is_succ_def Halpha); [trivial | ]. exists x; assumption. - destruct 1 as [beta [Hbeta H'beta]]; subst; now apply succ_is_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)