have : sgn p ≃ 0 := calc
  sgn p           ≃ _ := Rel.refl
  sgn p.numerator ≃ _ := Integer.sgn_zero.mp ‹p.numerator ≃ 0›
  0               ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
this : sgn p ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)