∀ (motive : (a b : ℤ) → b < 0 ∧ ¬b ∣ a → Prop) (a b : ℤ) (h : b < 0 ∧ ¬b ∣ a),
  (∀ (b : ℕ) (h : Int.negSucc b < 0 ∧ ¬Int.negSucc b ∣ 0), motive 0 (Int.negSucc b) h) →
    (∀ (a : ℕ) (h : Int.negSucc 0 < 0 ∧ ¬Int.negSucc 0 ∣ Int.ofNat (a + 1)),
        motive (Int.ofNat a.succ) (Int.negSucc 0) h) →
      (∀ (a b : ℕ) (h : Int.negSucc (b + 1) < 0 ∧ ¬Int.negSucc (b + 1) ∣ Int.ofNat (a + 1)),
          motive (Int.ofNat a.succ) (Int.negSucc b.succ) h) →
        (∀ (a b : ℕ) (h : Int.negSucc b < 0 ∧ ¬Int.negSucc b ∣ Int.negSucc a),
            motive (Int.negSucc a) (Int.negSucc b) h) →
          motive a b h