have
  : AA.OneOfThree
    (p.numerator ≃ 0)
    (Positive p.numerator)
    (Negative p.numerator)
  := (Integer.sign_trichotomy p.numerator).atLeastOne
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ 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)
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)