CHANGELOG entry.

CHANGELOG.md

@@ -16,6 +16,8 @@ Coq 8.12 and 8.13 are no longer supported by this release.
 - Rename `loopup_total_empty` → `lookup_total_empty`.
 - Let `naive_solver tac` fail if `tac` creates new evars. Before it would
   succeed with a proof that contains unresolved evars/shelved goals.
+- Add lemmas `Nat.mul_reg_{l,r}` for cancellation of multiplication on `nat`.
+  (Names are analogous to the `Z.` lemmas for Coq's standard library.)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).