proposition: Remark RDlim : dominates_from 1 (F_ (E0_succ alpha)) (F_ alpha).
proof: Proof. red;intros; rewrite F_succ_eqn. change (F_ alpha p) with (iterate (F_ alpha) 1 p); 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)