proposition: Remark RB : forall n, n < F_ alpha n.
proof: Proof. subst alpha. intro n. rewrite F_succ_eqn. destruct (Halpha beta). apply Lt_Succ. change n with (iterate (F_ beta) 0 n) at 1. apply iterate_lt;auto with arith. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)