. 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 _
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ ulp n b

n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a