have le_size_pred : m ≤ Nat.size x - 1 := Nat.le_pred_of_lt lt_size
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 hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m