have : sgn p ≄ sgn p := Integer.mul_sqrt1_neqv.mp ‹sgn p * sgn p ≃ -1›
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝³ : sgn p * sgn p ≃ -1
this✝² : Integer.Nonzero (-1)
this✝¹ : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this✝ : Integer.Sqrt1 (sgn (sgn p))
this : Integer.Sqrt1 (sgn p)
⊢ False
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : sgn (p * p) ≃ -1
this✝⁴ : sgn p * sgn p ≃ -1
this✝³ : Integer.Nonzero (-1)
this✝² : Integer.Nonzero (sgn p * sgn p)
left✝ right✝ : Integer.Nonzero (sgn p)
this✝¹ : Integer.Sqrt1 (sgn (sgn p))
this✝ : Integer.Sqrt1 (sgn p)
this : sgn p ≄ sgn p
⊢ False