From 4901b4b615e670ad21cb601c7e2c67c189e13b5d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 11:29:24 +0200
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d2cbb354..2a4ef466 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`).
-- 
GitLab