cases pn with
| mk p n =>
  simp [Int.normalize]
  cases Classical.em (p ≥ n) with
  | inl hpn =>
    simp [*]
    exact Int.IsCanonical.nonneg
  | inr hpn =>
    simp [*]
    exact Int.IsCanonical.nonpos
pn : ℕ × ℕ
⊢ IsCanonical (normalize pn)
no goals