diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 93d0ebef3c..2219a35f5d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -39,7 +39,14 @@
     `gt0_power_pos`, `norm_power_pos`, `lt0_norm_power_pos`,
     `power_posB`
   + lemmas `powere_posrM`, `powere_posAC`, `gt0_powere_pos`,
-    `powere_pos_eqy`, `eqy_powere_pos`, `powere_posD`, `powere_posB`
+    `powere_pos_eqy`, `eqy_powere_pos`, `powere_posD`
+
+- in `exp.v`:
+  + notation `` e `^?(r +? s) ``
+  + lemmas `expR_eq0`, `power_posN`
+  + definition `powere_posD_def`
+  + lemmas `powere_posD_defE`, `powere_posB_defE`, `add_neq0_powere_posD_def`,
+    `add_neq0_powere_posB_def`, `nneg_neq0_powere_posD_def`, `nneg_neq0_powere_posB_def`
 
 ### Changed
 
@@ -49,14 +56,23 @@
   
 - moved from `functions.v` to `classical_sets.v`: `subsetP`.
 
+- in `exp.v`:
+  + lemmas `power_pos_eq0`, `powere_pos_eq0`
+
 ### Renamed
 
 - in `boolp.v`:
   + `mextentionality` -> `mextensionality`
   + `extentionality` -> `extensionality`
+
 - in `exp.v`:
   + `expK` -> `expRK`
 
+- in `exp.v`:
+  + `power_pos_eq0` -> `power_pos_eq0_eq0`
+  + `power_pos_inv` -> `power_pos_invn`
+  + `powere_pos_eq0` -> powere_pos_eq0_eq0`
+
 ### Generalized
 
 - in `exp.v`: