d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1
d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } * star { re := x, im := y } = 1
simp [Zsqrtd.ext, IsPell, mul_comm]
no goals
d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1
ring_nf