English
For any d > 0, and any solution a to Pell, there exists b in {a, a^{-1}, -a, -a^{-1}} with 0 < b.x and 0 ≤ b.y, and a belongs to {b, b^{-1}, -b, -b^{-1}}.
Русский
Для любого d > 0 и любого решения Пелля существует элемент b в {a, a^{-1}, -a, -a^{-1}} с 0 < b.x и 0 ≤ b.y, причём a принадлежит {b, b^{-1}, -b, -b^{-1}}.
LaTeX
$$$\exists b\in \{a, a^{-1}, -a, -a^{-1}\}, 0 < b.x \land 0 \le b.y \land a\in\{b,b^{-1},-b,-b^{-1}\}$$$
Lean4
/-- If `a` is any solution, then one of `a`, `a⁻¹`, `-a`, `-a⁻¹` has
positive `x` and nonnegative `y`. -/
theorem exists_pos_variant (h₀ : 0 < d) (a : Solution₁ d) :
∃ b : Solution₁ d, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ ({b, b⁻¹, -b, -b⁻¹} : Set (Solution₁ d)) := by
refine
(lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩) <;>
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, x_neg, x_inv, y_neg,
y_inv, neg_pos, neg_nonneg, or_true] <;>
assumption
