cases Classical.em (p ≥ n) with
| inl hpn =>
  simp [*]
  exact Int.IsCanonical.nonneg
| inr hpn =>
  simp [*]
  exact Int.IsCanonical.nonpos
case mk
p n : ℕ
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
no goals