have : Negative x := Rational.sgn_negative.mpr this
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝ : sgn y ≃ 1
this : sgn x ≃ -1
⊢ Negative x
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝¹ : sgn y ≃ 1
this✝ : sgn x ≃ -1
this : Negative x
⊢ Negative x