case mp =>
  intro (_ : Negative x)
  show ∃ (y : ℚ), Positive y ∧ x ≃ -y
  have : sgn x ≃ -1 := Rational.sgn_negative.mp ‹Negative x›
  have : sgn (-x) ≃ 1 := calc
    sgn (-x) ≃ _ := Rational.sgn_compat_neg
    (-sgn x) ≃ _ := AA.subst₁ ‹sgn x ≃ -1›
    (-(-1))  ≃ _ := Integer.neg_involutive
    1        ≃ _ := Rel.refl
  have : Positive (-x) := Rational.sgn_positive.mpr ‹sgn (-x) ≃ 1›
  have : x ≃ -(-x) := Rational.eqv_symm Rational.neg_involutive
  exact Exists.intro (-x) (And.intro ‹Positive (-x)› ‹x ≃ -(-x)›)
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y
no goals