cases Nat.le_total (next n x) (2 ^ Nat.size x) with
| inl le => exact Nat.le_trans (trunc_le n (next n x)) le
| inr ge => exact Nat.le_of_eq (trunc_next_of_carry npos ge)
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
no goals