calc
  sgn a₁ ≃ _ := sgn_negative.mp ‹Negative a₁›
  (-1)   ≃ _ := Rel.symm (sgn_negative.mp ‹Negative a₂›)
  sgn a₂ ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
c✝ : Negative a₁
this : Negative a₂
⊢ sgn a₁ ≃ sgn a₂
no goals