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