have : x ≃ -((a : ℚ) / b) := calc
  x                ≃ _ := ‹x ≃ (-a) / b›
  (-a : ℚ) / b     ≃ _ := Rational.eqv_symm Rational.neg_scompatL_div
  (-((a : ℚ) / b)) ≃ _ := Rational.eqv_refl
ℚ : 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
ℚ : 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