Theorem: size_pow_mul (Fl/Lemmas.lean)

State before:
x : ℕ
h : 0 < x
k : ℕ
⊢ Nat.size (2 ^ k * x) = Nat.size x + k
Tactic:
rw [Nat.mul_comm, size_mul_pow h k]
State after:
no goals