have : y ≃ a / b := y_eqv_a_over_b
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x