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