English
Let a1 be a fundamental Pell solution for d and a any solution with x > 1 and y > 0. Then a.x * a1.y ≤ a.y * a1.x.
Русский
Пусть a1 — фундаментальное решение уравнения Пелля, а также любое решение a с x > 1 и y > 0. Тогда выполняется неравенство a.x · a1.y ≤ a.y · a1.x.
LaTeX
$$$\forall d \in \mathbb{Z},\; \forall a_1 \in \text{Solution}_1(d),\; \text{IsFundamental}(a_1) \Rightarrow \forall a \in \text{Solution}_1(d),\; 1 < a.x \Rightarrow 0 < a.y \Rightarrow a.x \cdot a_1.y \le a.y \cdot a_1.x.$$$
Lean4
theorem x_mul_y_le_y_mul_x {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
a.x * a₁.y ≤ a.y * a₁.x :=
by
rw [← abs_of_pos <| zero_lt_one.trans hax, ← abs_of_pos hay, ← abs_of_pos h.x_pos, ← abs_of_pos h.2.1, ← abs_mul, ←
abs_mul, ← sq_le_sq, mul_pow, mul_pow, a.prop_x, a₁.prop_x, ← sub_nonneg]
ring_nf
rw [sub_nonneg, sq_le_sq, abs_of_pos hay, abs_of_pos h.2.1]
exact h.y_le_y hax hay
