a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x) - ↑(Pell.d a1 * y * y) = ↑1
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x - Pell.d a1 * y * y) = ↑1
rw [Int.ofNat_sub (Int.le_of_ofNat_le_ofNat <| Int.le.intro_sub _ h)]
no goals
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x) - ↑(Pell.d a1 * y * y) = ↑1
exact h
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - Pell.d a1 * y * y = 1
⊢ ↑1 = 1
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - Pell.d a1 * y * y = 1
⊢ ↑(x * x) - ↑(Pell.d a1 * y * y) = 1
rw [← Int.ofNat_sub <| le_of_lt <| Nat.lt_of_sub_eq_succ h, h]
no goals
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - Pell.d a1 * y * y = 1
⊢ ↑1 = 1
rfl