What did Coq 8.15 change about divmod?

Question

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).

Answer 1

This was changed in Coq 8.14 (MR: https://github.com/coq/coq/pull/14086), and the changes are summarized in https://coq.inria.fr/refman/changes.html#id310. Quoting:

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.