have : Positive ((a : ℚ) / b) := alt_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)
⊢ 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)
⊢ Negative x