proposition: Remark N_simpl: N = exp2 70 - 1.
proof: Proof. change 70 with (64 + 6)%nat. assert (forall n p, (exp2 (n + p) = exp2 n * exp2 p)%nat). { induction n; cbn. intro p; now rewrite Nat.add_0_r. intros p; rewrite !Nat.add_0_r. repeat rewrite IHn; ring. } rewrite H; unfold N; reflexivity. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)