rw [Nat.left_distrib, Nat.two_mul, Nat.add_assoc,
    Nat.mul_div_cancel' ulp_even, ← ulp_trunc npos, next]
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)
no goals