proposition: Lemma H'_omega_sqr : forall k, H'_ (E0_phi0 2)%e0 k = (exp2 (S k ) * (S k) - 1)%nat.
proof: Proof. intro k; rewrite H'_eq3; auto with E0. - ochange (Canon (E0_phi0 2) (S k)) (E0_omega * (S k))%e0. + rewrite H'_omega_i; simpl (exp2 (S k)). * rewrite Nat.add_pred_r. -- abstract lia. -- generalize (exp2_not_zero k); abstract lia. + cbn; f_equal; abstract lia. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)