case mp =>
  intro (_ : Negative x)
  show AltNegative x
  have (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y))) :=
    negative_iff_neg_positive.mp ‹Negative x›
  have
    (AltPositive.intro
      (a : ℤ) (b : ℤ)
      (_ : AP (Positive a)) (_ : AP (Positive b)) y_eqv_a_over_b)
    := alt_positive.mp ‹Positive y›
  have : y ≃ a / b := y_eqv_a_over_b
  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
  exact AltNegative.mk this
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → AltNegative x
no goals