proposition: Lemma H'_Phi0_omega_exact_formula k : H'_ (E0_phi0 E0_omega) k = let F f i := iterate f (S i) i in let g k := S (2 * k)%nat in iterate F k g k.
proof: Proof. rewrite H'_Phi0_omega; unfold H'_succ_fun; apply iterate_ext2. - intro; now rewrite H'_omega. - intros; now apply iterate_ext. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)