have : Negative x := negative_iff_neg_positive.mpr 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)
this : ∃ y, Positive y ∧ x ≃ -y
⊢ 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
this : Negative x
⊢ Negative x