added lemma reflp_on_conversp[simp]

--- a/NEWS	Wed Nov 09 15:38:43 2022 +0100
+++ b/NEWS	Wed Nov 09 16:36:22 2022 +0100
@@ -45,6 +45,7 @@
       preorder.antisymp_less[simp]
       preorder.reflp_ge[simp]
       preorder.reflp_le[simp]
+      reflp_on_conversp[simp]
       totalp_on_singleton[simp]
 
 * Theory "HOL.Transitive_Closure":

--- a/src/HOL/Relation.thy	Wed Nov 09 15:38:43 2022 +0100
+++ b/src/HOL/Relation.thy	Wed Nov 09 16:36:22 2022 +0100
@@ -951,6 +951,9 @@
 lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
   by (auto simp: refl_on_def)
 
+lemma reflp_on_conversp [simp]: "reflp_on A R\<inverse>\<inverse> \<longleftrightarrow> reflp_on A R"
+  by (auto simp: reflp_on_def)
+
 lemma sym_converse [simp]: "sym (converse r) = sym r"
   unfolding sym_def by blast