. exact size_next_le_succ_size n x
case h₁
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) ≤ Nat.size x + 1

case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)