apply size_div_mul
case inr
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ 2 ^ (Nat.size x - n) ≤ x