added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]

--- a/NEWS	Thu Oct 13 17:00:43 2022 +0200
+++ b/NEWS	Thu Oct 13 17:22:34 2022 +0200
@@ -20,6 +20,10 @@
       antisymp_if_asymp
       irreflD
       irreflpD
+      linorder.totalp_ge[simp]
+      linorder.totalp_greater[simp]
+      linorder.totalp_le[simp]
+      linorder.totalp_less[simp]
       order.antisymp_ge[simp]
       order.antisymp_le[simp]
       preorder.antisymp_greater[simp]

--- a/src/HOL/Relation.thy	Thu Oct 13 17:00:43 2022 +0200
+++ b/src/HOL/Relation.thy	Thu Oct 13 17:22:34 2022 +0200
@@ -593,6 +593,18 @@
 lemma totalp_on_singleton [simp]: "totalp_on {x} R"
   by (simp add: totalp_on_def)
 
+lemma (in linorder) totalp_less[simp]: "totalp_on A (<)"
+  by (auto intro: totalp_onI)
+
+lemma (in linorder) totalp_greater[simp]: "totalp_on A (>)"
+  by (auto intro: totalp_onI)
+
+lemma (in linorder) totalp_le[simp]: "totalp_on A (\<le>)"
+  by (rule totalp_onI, rule linear)
+
+lemma (in linorder) totalp_ge[simp]: "totalp_on A (\<ge>)"
+  by (rule totalp_onI, rule linear)
+
 
 subsubsection \<open>Single valued relations\<close>