have : sgn (-x) ≃ 1 := calc
  sgn (-x) ≃ _ := Rational.sgn_compat_neg
  (-sgn x) ≃ _ := AA.subst₁ ‹sgn x ≃ -1›
  (-(-1))  ≃ _ := Integer.neg_involutive
  1        ≃ _ := Rel.refl
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this : sgn x ≃ -1
⊢ ∃ y, Positive y ∧ x ≃ -y
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝ : sgn x ≃ -1
this : sgn (-x) ≃ 1
⊢ ∃ y, Positive y ∧ x ≃ -y