English
For a Pell solution with x and y positive, the y-coordinate of a^n is positive for every integer exponent n.
Русский
Для решения Пелля с x,y положительными, y-координата a^n положительна для всякого целочисленного показательa n.
LaTeX
$$$\forall a\in \mathrm{Solution}_1(d),\; a_x>0 \land a_y>0 \rightarrow \forall n\in \mathbb{Z},\; (a^n)_y > 0$$$
Lean4
/-- If `(x, y)` is a solution with `x` and `y` positive, then all its powers with positive
exponents have positive `y`. -/
theorem y_zpow_pos {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) {n : ℤ} (hn : 0 < n) : 0 < (a ^ n).y :=
by
lift n to ℕ using hn.le
norm_cast at hn ⊢
rw [← Nat.succ_pred_eq_of_pos hn]
exact y_pow_succ_pos hax hay _
