rewrite [← Nat.pow_div lt_size.le two_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 ^ (Nat.size x - m) * 2 ^ 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 / 2 ^ m * 2 ^ m