∀ (motive : ℤ → ℤ → Sort u_1) (m : ℕ) (n : ℤ) (h_1 : (m : ℕ) → (n : ℤ) → motive (Int.ofNat m) n)
  (h_2 : (m : ℕ) → (n : ℤ) → motive (Int.negSucc m) n),
  (match Int.negSucc m, n with
    | Int.ofNat m, n => h_1 m n
    | Int.negSucc m, n => h_2 m n) =
    h_2 m n