rewrite [Nat.div_lt_iff_lt_mul two_pow_pos]
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ (Nat.size x - m) * 2 ^ m