∀ (motive : ℤ → ℤ → Prop) (x y : ℤ),
  (∀ (x y : ℕ), motive (Int.ofNat x) (Int.ofNat y)) →
    (∀ (x y : ℕ), motive (Int.ofNat x) (Int.negSucc y)) →
      (∀ (x y : ℕ), motive (Int.negSucc x) (Int.ofNat y)) →
        (∀ (x y : ℕ), motive (Int.negSucc x) (Int.negSucc y)) → motive x y