case succ k h_ind =>
  conv =>
    lhs; simp; change (n * (2^k*2)) >>> k / 2
    rw [Nat.mul_comm (2^k) 2, ←Nat.mul_assoc]
    rw [←Nat.shiftLeft_eq (n*2) k, h_ind (n*2), Nat.mul_div_cancel n (n:=2) (by decide)]
k : Nat
h_ind : ∀ (n : Nat), n <<< k >>> k = n
n : Nat
⊢ n <<< succ k >>> succ k = n
no goals