have : Positive (-x) := Rational.sgn_positive.mpr ‹sgn (-x) ≃ 1›
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝ : sgn x ≃ -1
this : sgn (-x) ≃ 1
⊢ ∃ y, Positive y ∧ x ≃ -y
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝¹ : sgn x ≃ -1
this✝ : sgn (-x) ≃ 1
this : Positive (-x)
⊢ ∃ y, Positive y ∧ x ≃ -y