# What did Coq 8.15 change about divmod?

I noticed that Coq 8.15 (possibly 8.14) made some significant changes to divmod. In particular, Nat.divmod_0q0 seems to have been removed and the div_mod lemma with signature y<>0 -> x = y*(x/y) + x mod y has effectively been replaced with div_mod_eq which drops the y<>0 precondition.

Does divmod (and hence div and mod) now behave differently? Could somebody summarize the changes? It looks like some 8.15 theorems simply don't hold in 8.13 and vice-versa (with Nat.divmod_0q0).

Changed: set n mod 0 = n uniformly for nat, N, Z, int63, sint63, int31 such that m = (m / n) * n + (m mod n) holds (also for n = 0)
As you can see, in many cases this gives stronger theorems with fewer side conditions — but in any case they're more uniform across nat, N and Z.