English
If a is a Pell solution with x > 0, then for every integer exponent n, the x-coordinate of a^n is positive.
Русский
Если у решения Пелля x > 0, то для любого целочисленного показателя n x-координата a^n положительна.
LaTeX
$$$\forall a\in \mathrm{Solution}_1(d),\; a_x>0 \rightarrow \forall n\in \mathbb{Z},\; (a^n)_x > 0$$$
Lean4
/-- If `(x, y)` is a solution with `x` positive, then all its powers have positive `x`. -/
theorem x_zpow_pos {a : Solution₁ d} (hax : 0 < a.x) (n : ℤ) : 0 < (a ^ n).x := by
cases n with
| ofNat n =>
rw [Int.ofNat_eq_coe, zpow_natCast]
exact x_pow_pos hax n
| negSucc n =>
rw [zpow_negSucc]
exact x_pow_pos hax (n + 1)