∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive (m + 1) (n + 1)) (m n : ℕ),
  Nat.casesDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n