intro (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y)))
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ Negative x