have : x ≃ (-a) / b := calc
  x                ≃ _ := ‹x ≃ -y›
  (-y)             ≃ _ := Rational.neg_subst ‹y ≃ a / b›
  (-((a : ℚ) / b)) ≃ _ := Rational.neg_scompatL_div
  (-a : ℚ) / b     ≃ _ := Rational.eqv_refl
ℚ : 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
ℚ : 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
this : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x