have
  (AltNegative.intro
    (a : ℤ) (b : ℤ)
    (_ : AP (Positive a)) (_ : AP (Positive b)) x_eqv_neg_a_over_b)
  := ‹AltNegative x›
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
⊢ 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 : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ Negative x