added lemma refl_lex_prod[simp]

--- a/NEWS	Mon Dec 19 12:00:15 2022 +0100
+++ b/NEWS	Mon Dec 19 12:00:56 2022 +0100
@@ -124,6 +124,7 @@
       asym_on_lex_prod[simp]
       irrefl_lex_prod[simp]
       irrefl_on_lex_prod[simp]
+      refl_lex_prod[simp]
       sym_lex_prod[simp]
       sym_on_lex_prod[simp]
       wfP_if_convertible_to_nat

--- a/src/HOL/Wellfounded.thy	Mon Dec 19 12:00:15 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 19 12:00:56 2022 +0100
@@ -849,6 +849,9 @@
     by (simp add: zeq)
 qed auto
 
+lemma refl_lex_prod[simp]: "refl r\<^sub>B \<Longrightarrow> refl (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (auto intro!: reflI dest: refl_onD)
+
 lemma irrefl_on_lex_prod[simp]:
   "irrefl_on A r\<^sub>A \<Longrightarrow> irrefl_on B r\<^sub>B \<Longrightarrow> irrefl_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
   by (auto intro!: irrefl_onI dest: irrefl_onD)