rewrite [tsub_le_iff_tsub_le]
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - n ≤ Nat.size x
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - Nat.size x ≤ n