conv =>
  lhs; rw [Nat.mul_succ 2 n]; unfold log2'; rw [recBase2_div2]
  change log2' (2*n/2 + 1) + 1
  rw [Nat.mul_div_right n (Nat.zero_lt_succ 1)]
n : Nat
⊢ log2' (2 * succ n) = log2' (succ n) + 1
no goals