proposition: Remark RClim : F_ alpha <<= F_ (E0_succ alpha).
proof: Proof. intro n; destruct n. - repeat rewrite F_alpha_0_eq; auto with arith. - apply Nat.lt_le_incl; rewrite F_succ_eqn. change (F_ alpha (S n)) with (iterate (F_ alpha) 1 (S n)). apply iterate_lt. + apply RAlim. + red;intros; apply RBlim. + auto with arith. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)