cases Nat.lt_or_ge (next n x) (2 ^ Nat.size x) with
| inl next_lt => exact trunc_next_comm_of_no_carry npos next_lt
| inr next_ge => rw [next_trunc_of_carry npos next_ge, trunc_next_of_carry npos next_ge]
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) = next n (trunc n x)
no goals