apply Nat.le_antisymm
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) = Nat.size x
case h₁
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) ≤ Nat.size x

case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)