rw [← pow_add, size_pow_mul pos, ← tsub_add_eq_add_tsub h, Nat.add_comm]
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
pos : 0 < x
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
no goals