diff --git a/CHANGELOG.md b/CHANGELOG.md
index d2cbb354e653e0e7714fbacab37686fb365c5ca5..2a4ef466067887247d5504b05beadd5ad930c364 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,8 @@ API-breaking change is listed.
   and an assumption `R' x y` is found, we search for an instance of
   `SolveProperSubrelation R' R` and if we find one, that finishes the proof.
 - Remove `wf` alias for the standard `well_founded`.
+- Add lemmas `Nat.lt_wf_0_projected`, `N.lt_wf_0_projected`, `Z.lt_wf_projected`
+  for easy measure/size induction.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).