. apply add_lt_add_of_lt_of_le
  . exact Nat.lt_size_self x
  . apply ulp_le_ulp
    exact Nat.le_add_right x (2 ^ expt n x)
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
no goals