proposition: Lemma H'_Phi0_omega : forall k, H'_ (E0_phi0 E0_omega) k = iterate H'_succ_fun k (H'_ E0_omega) k.
proof: Proof. Proof with auto with E0. intro k; rewrite H'_eq3, <- H'_Phi0_Si ... - rewrite CanonS_phi0_lim; f_equal ... Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)