apply Nat.pow_le_pow_of_le_right two_pos
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ 2 ^ (Nat.size y - n) ≤ 2 ^ (Nat.size x - n)
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ Nat.size y - n ≤ Nat.size x - n