apply Iff.intro
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x ↔ ∃ y, Positive y ∧ x ≃ -y
case mp
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x