proposition: Remark R3 : F_ (E0_succ alpha) (S n)= F_ alpha (iterate (F_ alpha) (S n) (S n)).
proof: Proof. rewrite F_succ_eqn; now rewrite iterate_S_eqn. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)