feat(number_theory/pell): add API for solutions (#18626)
This continues the devlopment of the theory of Pell's equation.
We add some API lemmas for solutions, which will be needed for defining of the fundamental solution and proving its properties.
See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Proving.20Pell's.20equation.20is.20solvable/near/343270338).
