proposition: Lemma H'_Omega_term_0 (alpha : E0) : alpha <> E0zero -> forall i k, H'_ (Omega_term alpha i) k = iterate (H'_ (E0_phi0 alpha)) (S i) k.
proof: Proof. induction i. - reflexivity. - intros; rewrite H'_Omega_term_1, IHi; trivial; now rewrite <- iterate_rw. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)