. unfold expt
  rewrite [size_next_eq_succ_size_of_carry carry]
  rewrite [tsub_le_iff_tsub_le]
  rewrite [add_tsub_cancel_left]
  exact Nat.one_le_of_lt npos
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ expt n (next n x) ≤ Nat.size x

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