cases Nat.eq_zero_or_pos x with
| inl zero => rw [zero, Nat.zero_div, Nat.zero_mul]
| inr pos =>
  apply size_div_mul
  rewrite [← Nat.lt_size]
  exact tsub_lt_self (Nat.size_pos.mpr pos) npos
n : ℕ
npos : 0 < n
x : ℕ
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
no goals