simpa using h.mul (FiniteField.isSquare_neg_one_iff.2 hF)
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : Fintype.card F % 4 ≠ 3
x✝¹ x✝ : F
h : (fun x y => IsSquare (x - y)) x✝¹ x✝
⊢ (fun x y => IsSquare (x - y)) x✝ x✝¹
no goals