proposition: Remark F_3_eqn : forall n, F_ 3 n = iterate (F_ 2) (S n) n.
proof: Proof. intro n; ochange (E0fin 3) (E0_succ (E0fin 2)); now rewrite F_succ_eqn. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)