proposition: Remark RBlim : forall n, n < F_ alpha n.
proof: Proof. intro n. rewrite F_lim_eqn. destruct (Halpha (Canon alpha n)). apply Canon_lt. now apply Limit_not_Zero. auto. auto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)