rewrite [Nat.two_mul, ← tsub_le_iff_right, tsub_right_comm, tsub_le_iff_left]
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 - trunc n (b - a) ≤ 2 * a
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