calc
  b - a ≤ next n (trunc n (b - a))    := Nat.le_of_lt $ lt_next_trunc npos _
  _ = trunc n (b - a) + ulp n (b - a) := by unfold next ; rw [ulp_trunc npos _]
  _ ≤ trunc n (b - a) + ulp n b       := Nat.add_le_add_left (ulp_le_ulp n tsub_le_self) _
  _ ≤ trunc n (b - a) + a             := Nat.add_le_add_left ulp_le _
case inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ b - a ≤ trunc n (b - a) + a
no goals