proposition: Fact F1_simpl : H'_ (E0_phi0 3) 3 = (exp2 (exp2 (S N) * S N) * (exp2 (S N) * S N) - 1)%nat.
proof: Proof. rewrite F1; unfold f. assert (forall k, k <> 0 -> (S (k -1) = k)%nat) by lia. rewrite (H (exp2 (S N) * S N)%nat). - reflexivity. - apply Nat.neq_mul_0; split. + apply exp2_not_zero. + discriminate. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)