Theorem: trunc_next_comm_of_no_carry (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
no_carry : next n x < 2 ^ Nat.size x
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
rw [trunc_next_of_no_carry no_carry, next, ulp_trunc npos x]
State after:
no goals