unfold next
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ next n (trunc n (b - a)) = trunc n (b - a) + ulp n (b - a)
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ trunc n (b - a) + ulp n (trunc n (b - a)) = trunc n (b - a) + ulp n (b - a)