apply Nat.pow_le_pow_of_le_right two_pos
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - n) ≤ 2 ^ (Nat.size (a - b) - n)
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ Nat.size a - n ≤ Nat.size (a - b) - n