rewrite [← trunc_next_comm npos (trunc n x - 1)]
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = next n (trunc n (trunc n x - 1))
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (next n (trunc n x - 1))