English
If a1 is fundamental and a is a solution with 1 < a.x and a.y > 0, then the y-coordinate of a a1^{-1} is nonnegative: (a a1^{-1}).y ≥ 0.
Русский
Если a1 — фундаментальное решение, а a — решение с 1 < a.x и a.y > 0, то y-координата произведения a a1^{-1} неотрицательна: (a a1^{-1}).y ≥ 0.
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 0 \le (a \cdot a_1^{-1}).y.$$$
Lean4
/-- If we multiply a positive solution with the inverse of a fundamental solution,
the `y`-coordinate remains nonnegative. -/
theorem mul_inv_y_nonneg {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
0 ≤ (a * a₁⁻¹).y := by
simpa only [y_inv, mul_neg, y_mul, le_neg_add_iff_add_le, add_zero] using h.x_mul_y_le_y_mul_x hax hay
