rw [trunc, ulp_next_of_no_carry no_carry, next, trunc, ← Nat.succ_mul,
    Nat.add_div_right _ (ulp_pos n x)]
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ trunc n (next n x) = trunc n x + ulp n x
no goals