cases Nat.le_total a (ulp n b) with
| inl le_ulp => trans ulp n b
  . rewrite [tsub_le_iff_tsub_le]
    calc
      b - ulp n b
      _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
      _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
  . exact h
| inr ulp_le => rewrite [Nat.two_mul, ← tsub_le_iff_right, tsub_right_comm, tsub_le_iff_left]
  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 _
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
⊢ b - trunc n (b - a) ≤ 2 * a
no goals