rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) ∣ 2 ^ k
case h
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
⊢ Nat.size (2 ^ k * x) - n ≤ k