have : sgn y ≃ 1 := Rational.sgn_positive.mp ‹Positive y›
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ Negative x
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this : sgn y ≃ 1
⊢ Negative x