proposition: Corollary F_alpha_positive alpha : forall n, 0 < F_ alpha n.
proof: Proof. intro n; apply Nat.le_lt_trans with n; auto with arith. apply F_alpha_gt. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)