Theorem: arb_large_soln (IIScExperiments/NumberTheory3.lean)

State before:
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ 5 ∣ 4 * n ^ 2 + 1 ∧ 13 ∣ 4 * n ^ 2 + 1
Tactic:
sorry
State after:
no goals