--- a/NEWS Thu Feb 23 12:31:46 2023 +0100
+++ b/NEWS Thu Feb 23 12:35:37 2023 +0100
@@ -218,6 +218,7 @@
asymp_not_liftable_to_multpHO
irreflp_on_multpHO[simp]
multpDM_mono_strong
+ multpDM_plus_plusI[simp]
multpHO_mono_strong
multpHO_plus_plus[simp]
totalp_multpDM