# HG changeset patch
# User desharna
# Date 1665479227 -7200
# Node ID 61a5b5ad3a6e3ef33dbe9c04aa416431b765afe9
# Parent  207b6fcfc47df9b0b74a76016783df414542fd33
added lemmas reflp_ge[simp] and reflp_le[simp]

diff -r 207b6fcfc47d -r 61a5b5ad3a6e NEWS
--- a/NEWS	Mon Oct 10 19:07:54 2022 +0200
+++ b/NEWS	Tue Oct 11 11:07:07 2022 +0200
@@ -16,6 +16,8 @@
       antisymp_if_asymp
       irreflD
       irreflpD
+      reflp_ge[simp]
+      reflp_le[simp]
       totalp_on_singleton[simp]
 
 
diff -r 207b6fcfc47d -r 61a5b5ad3a6e src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Oct 10 19:07:54 2022 +0200
+++ b/src/HOL/Relation.thy	Tue Oct 11 11:07:07 2022 +0200
@@ -256,6 +256,12 @@
 lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp Q"
   by (rule reflp_on_mono[of UNIV R Q]) simp_all
 
+lemma (in preorder) reflp_le[simp]: "reflp (\<le>)"
+  by (simp add: reflpI)
+
+lemma (in preorder) reflp_ge[simp]: "reflp (\<ge>)"
+  by (simp add: reflpI)
+
 
 subsubsection \<open>Irreflexivity\<close>