rewrite [tsub_le_iff_tsub_le]
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
⊢ b - ulp n b ≤ trunc n (b - a)