have pos : 0 < x := by
  rewrite [← Nat.size_pos]
  exact Nat.lt_of_lt_of_le npos h
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
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)