have : a₂ ≃ 0 := AA.substLFn ‹a₁ ≃ a₂› ‹a₁ ≃ 0›
ℕ : 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₁)
a✝ : a₁ ≃ 0
⊢ sgn a₁ ≃ sgn a₂
ℕ : 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₁)
a✝ : a₁ ≃ 0
this : a₂ ≃ 0
⊢ sgn a₁ ≃ sgn a₂