∀ (motive : (k : ℕ) → (i : ℤ) → i ≠ 0 → i.natAbs ≤ k → ℕ → ℕ → Prop),
  (∀ (i : ℤ) (hi : i ≠ 0) (acc k : ℕ) (x : k + 1 ≠ 0) (hk : i.natAbs ≤ k + 1) (h : i % 2 = 0),
      motive k (i / 2) ⋯ ⋯ (acc + 1) (Int.trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1)) →
        motive k.succ i hi hk acc (Int.trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1))) →
    (∀ (i : ℤ) (hi : i ≠ 0) (acc k : ℕ),
        k + 1 ≠ 0 → ∀ (hk : i.natAbs ≤ k + 1), ¬i % 2 = 0 → motive k.succ i hi hk acc acc) →
      ∀ (k : ℕ) (i : ℤ) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : ℕ),
        motive k i hi hk acc (Int.trailingZeros.aux k i hi hk acc)