∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (m = 0 → False) →
    (match Int.ofNat m, Int.ofNat n with
      | 0, x => h_1 x
      | Int.ofNat m, Int.ofNat n => h_2 m n
      | Int.ofNat m.succ, Int.negSucc n => h_3 m n
      | Int.negSucc m, Int.ofNat n => h_4 m n
      | Int.negSucc m, Int.negSucc n => h_5 m n) =
      h_2 m n