have : sgn x ≃ -1 := Rational.sgn_negative.mp ‹Negative x›
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ ∃ y, Positive y ∧ x ≃ -y
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this : sgn x ≃ -1
⊢ ∃ y, Positive y ∧ x ≃ -y