English
Let a1 be a fundamental Pell solution for d and a a solution with 1 < a.x and a.y > 0. Then the x-coordinate strictly decreases when multiplied by the inverse of a1: (a a1^{-1}).x < a.x.
Русский
Пусть a1 — фундаментальное решение Пелля, а a — решение с 1 < a.x и a.y > 0. Тогда x-координата после умножения на обратное a1 строго уменьшается: (a a1^{-1}).x < a.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 (a \cdot a_1^{-1}).x < a.x.$$$
Lean4
/-- If we multiply a positive solution with the inverse of a fundamental solution,
the `x`-coordinate decreases. -/
theorem mul_inv_x_lt_x {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
(a * a₁⁻¹).x < a.x := by
simp only [x_mul, x_inv, y_inv, mul_neg, add_neg_lt_iff_le_add']
refine lt_of_mul_lt_mul_left ?_ h.2.1.le
calc
a₁.y * (a.x * a₁.x)
_ = a.x * a₁.y * a₁.x := by ring
_ ≤ a.y * a₁.x * a₁.x := by have := h.1; have := x_mul_y_le_y_mul_x h hax hay; gcongr
rw [mul_assoc, ← sq, a₁.prop_x, ← sub_neg]
suffices a.y - a.x * a₁.y < 0 by convert this using 1; ring
rw [sub_neg, ← abs_of_pos hay, ← abs_of_pos h.2.1, ← abs_of_pos <| zero_lt_one.trans hax, ← abs_mul, ← sq_lt_sq,
mul_pow, a.prop_x]
calc
a.y ^ 2 = 1 * a.y ^ 2 := (one_mul _).symm
_ ≤ d * a.y ^ 2 := ((mul_le_mul_iff_left₀ <| sq_pos_of_pos hay).mpr h.d_pos)
_ < d * a.y ^ 2 + 1 := (lt_add_one _)
_ = (1 + d * a.y ^ 2) * 1 := by rw [add_comm, mul_one]
_ ≤ (1 + d * a.y ^ 2) * a₁.y ^ 2 :=
(mul_le_mul_iff_right₀ (by have := h.d_pos; positivity)).mpr (sq_pos_of_pos h.2.1)
