English
If a is a fundamental Pell solution, then (a^m).y < (a^n).y holds exactly when m < n.
Русский
Если a — фундаментальное решение Пелля, то (a^m).y < (a^n).y тогда и только если m < n.
LaTeX
$$$\forall a\in \mathrm{Solution}_1(d),\; \text{IsFundamental}(a) \rightarrow \forall m,n\in \mathbb{Z},\; (a^m).y < (a^n).y \iff m < n$$$
Lean4
/-- If there is a fundamental solution, it is unique. -/
theorem subsingleton {a b : Solution₁ d} (ha : IsFundamental a) (hb : IsFundamental b) : a = b :=
by
have hx := le_antisymm (ha.2.2 hb.1) (hb.2.2 ha.1)
refine Solution₁.ext hx ?_
have : d * a.y ^ 2 = d * b.y ^ 2 := by rw [a.prop_y, b.prop_y, hx]
exact (sq_eq_sq₀ ha.2.1.le hb.2.1.le).mp (Int.eq_of_mul_eq_mul_left ha.d_pos.ne' this)
