have ulp_even := two_dvd_ulp_of_no_uflow no_uflow
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
ulp_even : 2 ∣ ulp n x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)