have (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y))) :=
  negative_iff_neg_positive.mp ‹Negative x›
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ AltNegative x
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ AltNegative x