∀ (k : ℕ) (i : ℤ) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : ℕ),
  Int.trailingZeros.aux k i hi hk acc =
    match k, ⋯, hk with
    | k.succ, x, hk => if h : i % 2 = 0 then Int.trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1) else acc