Theorem: Nat.log2'_mul2 (Algdata/Data/Nat/Bits.lean)

State before:
n : Nat
⊢ log2' (2 * succ n) = log2' (succ n) + 1
Tactic:
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)]
State after:
no goals