added lemma reflp_on_mono[mono]

--- a/NEWS	Mon Mar 24 13:59:08 2025 +0100
+++ b/NEWS	Mon Mar 24 14:04:11 2025 +0100
@@ -71,6 +71,7 @@
       left_unique_mono[mono]
       left_unique_mono_strong
       refl_on_top[simp]
+      reflp_on_mono[mono]
       reflp_on_refl_on_eq[pred_set_conv]
       reflp_on_top[simp]
       right_unique_mono[mono]

--- a/src/HOL/Relation.thy	Mon Mar 24 13:59:08 2025 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 24 14:04:11 2025 +0100
@@ -261,6 +261,9 @@
   "reflp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
   by (rule reflp_onI) (auto dest: reflp_onD)
 
+lemma reflp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> reflp_on B R \<le> reflp_on A Q"
+  by (simp add: reflp_on_mono_strong le_fun_def)
+
 lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp Q"
   using reflp_on_mono_strong[OF _ subset_UNIV] .