. rewrite [← add_tsub_assoc_of_le le_ulp]
  apply tsub_le_tsub_right
  apply add_le_of_dvd_of_dvd_of_lt
  . exact ulp_dvd_of_trunc_eq hfa
  . unfold ulp expt
    rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
    apply tsub_le_tsub_left
    exact Nat.one_le_of_lt npos
  . exact size_lt
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 - 1) + (ulp n a - b) ≤ a - b
no goals