have : ∃ (y : ℚ), Positive y ∧ x ≃ -y :=
  Exists.intro ((a : ℚ) / b) (And.intro ‹Positive ((a : ℚ) / b)› this)
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝² : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝¹ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝ : Positive (Rational.from_integer a / Rational.from_integer b)
this : x ≃ -(Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝³ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝² : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : Positive (Rational.from_integer a / Rational.from_integer b)
this✝ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this : ∃ y, Positive y ∧ x ≃ -y
⊢ Negative x