# HG changeset patch
# User desharna
# Date 1665674554 -7200
# Node ID 8e777e0e206a83212e8ff6caea48947f54f49950
# Parent  71bf371a97844d3cd85fd6793faeb80645b70dee
added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]

diff -r 71bf371a9784 -r 8e777e0e206a NEWS
--- 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]
diff -r 71bf371a9784 -r 8e777e0e206a src/HOL/Relation.thy
--- 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>