conv =>
  lhs; change getBit ((2 * n <<< k.pred) / 2) i
  rw [Nat.mul_div_cancel_left _ (Nat.zero_lt_succ 1)]
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) (succ i) = false
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< pred k) i = false