proposition: Lemma HFsucc : E0is_succ alpha -> P alpha.
proof: Proof. intro H; destruct (Succb_Succ _ H) as [beta Hbeta]; subst. intro n; rewrite H'_Phi0_succ. unfold H'_succ_fun; rewrite F_succ_eqn. specialize (IHalpha beta (Lt_Succ beta)); unfold P in IHalpha. - apply iterate_mono_1 with 1. + apply F_alpha_mono. + intro k; apply F_alpha_gt. + intros; destruct n0. * lia. * apply IHalpha. + lia. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)