. apply Nat.pow_le_pow_of_le_right two_pos
  exact tsub_le_tsub_left (Nat.one_le_of_lt npos) _
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ 2 ^ (Nat.size x - 1)

n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x