apply add_lt_add_of_lt_of_le
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)
case a.h₁
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x < 2 ^ Nat.size x

case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)