proposition: Lemma H'_F alpha : forall n, F_ alpha (S n) <= H'_ (E0_phi0 alpha) (S n).
proof: Proof. pattern alpha; apply well_founded_induction with E0lt. - apply E0lt_wf. - clear alpha; intros alpha IHalpha. destruct (Zero_Limit_Succ_dec alpha) as [[Hzero | Hlim] | Hsucc]. + subst; apply HF0. + apply HFLim; auto. + destruct Hsucc; subst; apply HFsucc. intros; apply IHalpha; auto. apply Succ_Succb. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)