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