have : sgn x ≃ -1 := calc
  sgn x      ≃ _ := Rational.sgn_subst ‹x ≃ -y›
  sgn (-y)   ≃ _ := Rational.sgn_compat_neg
  (-(sgn y)) ≃ _ := AA.subst₁ ‹sgn y ≃ 1›
  (-1)       ≃ _ := Rel.refl
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this : sgn y ≃ 1
⊢ Negative x
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝ : sgn y ≃ 1
this : sgn x ≃ -1
⊢ Negative x