have lt_size : m < Nat.size x := by rwa [Nat.lt_size]
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m