. have le_size_pred : m ≤ Nat.size x - 1 := Nat.le_pred_of_lt lt_size
  rewrite [tsub_right_comm]
  rewrite [← Nat.pow_div le_size_pred two_pos]
  apply Nat.div_le_div_right
  exact le_size_of_pos pos
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m

case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < 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
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)