calc
  sgn p             ≃ _ := sgn_subst ‹p ≃ 0›
  sgn ((0 : ℤ) : ℚ) ≃ _ := sgn_from_integer
  sgn (0 : ℤ)       ≃ _ := Integer.sgn_zero.mp Rel.refl
  0                 ≃ _ := Rel.refl
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
x✝ : p ≃ 0
⊢ sgn p ≃ 0
no goals