--- a/NEWS Mon Dec 19 08:01:31 2022 +0100
+++ b/NEWS Mon Dec 19 08:07:36 2022 +0100
@@ -43,6 +43,8 @@
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
order.antisymp_le[simp] ~> order.antisymp_on_le[simp]
+ preorder.asymp_greater[simp] ~> preorder.asymp_on_greater[simp]
+ preorder.asymp_less[simp] ~> preorder.asymp_on_less[simp]
preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
reflp_equality[simp] ~> reflp_on_equality[simp]