exact AA.OneOfThree.first this
ℕ : 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)
no goals