proposition: Remark R4 : F_ (E0_succ alpha) n < iterate (F_ alpha) (S n) (S n).
proof: Proof. rewrite F_succ_eqn; apply iterate_mono; auto with arith. - apply F_alpha_mono. - intro; apply F_alpha_gt. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)