--- a/NEWS Mon May 08 11:26:04 2023 +0200
+++ b/NEWS Mon May 08 11:27:03 2023 +0200
@@ -245,6 +245,7 @@
- Added lemmas.
asymp_multpHO
asymp_not_liftable_to_multpHO
+ asymp_on_multpHO
irreflp_on_multpHO[simp]
multpDM_mono_strong
multpDM_plus_plusI[simp]