conv =>
  lhs; change (n <<< (k+1)).getBit i
  rw [Nat.add_comm, ←Nat.shiftLeft_shiftLeft]
  rw [h_ind (n <<< 1) (Nat.le_of_succ_le h), this]
  change ((2*n)/2).getBit (i-k.succ)
  simp
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
this : i - k = succ (i - succ k)
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
no goals