mathlib

5b05c634 - feat(number_theory/pell): add exists_pos_of_not_is_square (#18567)

feat(number_theory/pell): add exists_pos_of_not_is_square (#18567) This PR continues work on the theory of the Pell equation for general (nonsquare and positive) `d`. In preparation for proving statements on the structure of the solution set, this adds ```lean lemma exists_pos_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬ is_square d) : ∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ 1 < x ∧ 0 < y := ... ``` as a prerequisite for defining the fundamental solution as the solution with smallest `x > 1` and positive `y`. See [this thread on Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Proving.20Pell's.20equation.20is.20solvable/near/338175458).