have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝ : NonzeroWithSign a s
this : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a (-1)
⊢ Positive a ∨ Negative a
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a (-1)
this : Negative a
⊢ Positive a ∨ Negative a