proposition: Lemma H'_omega_3 k : H'_ (E0_omega * 3)%e0 k = (8 * k + 7)%nat.
proof: Proof. rewrite H'_eq3 ; [| reflexivity]. ochange (Canon (E0_omega * 3)%e0 (S k)) (E0_omega * 2 + E0finS k)%e0. rewrite FinS_eq, H'_Plus_Fin, H'_omega_double; abstract lia. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)