∀ (motive : (b : ℤ) → b ≠ 0 → Prop) (b : ℤ) (hb : b ≠ 0),
  (∀ (b : ℕ) (x : Int.ofNat (b + 1) ≠ 0), motive (Int.ofNat b.succ) x) →
    (∀ (b : ℕ) (x : Int.negSucc b ≠ 0), motive (Int.negSucc b) x) → motive b hb