unfold next
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n (trunc n x) = 2 ^ Nat.size x
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n x + ulp n (trunc n x) = 2 ^ Nat.size x