diff -r e321569ec7a1 -r b6b7f3caa74a src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Dec 19 11:25:37 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 19 11:26:56 2022 +0100
@@ -864,6 +864,14 @@
   "sym r\<^sub>A \<Longrightarrow> sym r\<^sub>B \<Longrightarrow> sym (r\<^sub>A <*lex*> r\<^sub>B)"
   by (rule sym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
 
+lemma asym_on_lex_prod[simp]:
+  "asym_on A r\<^sub>A \<Longrightarrow> asym_on B r\<^sub>B \<Longrightarrow> asym_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (auto intro!: asym_onI dest: asym_onD)
+
+lemma asym_lex_prod[simp]:
+  "asym r\<^sub>A \<Longrightarrow> asym r\<^sub>B \<Longrightarrow> asym (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule asym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
+
 text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
 lemma trans_lex_prod [simp,intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
   unfolding trans_def lex_prod_def by blast
@@ -875,9 +883,6 @@
 lemma total_lex_prod[simp]: "total r\<^sub>A \<Longrightarrow> total r\<^sub>B \<Longrightarrow> total (r\<^sub>A <*lex*> r\<^sub>B)"
   by (rule total_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
 
-lemma asym_lex_prod: "\<lbrakk>asym R; asym S\<rbrakk> \<Longrightarrow> asym (R <*lex*> S)"
-  by (auto simp add: asym_iff lex_prod_def)
-
 text \<open>lexicographic combinations with measure functions\<close>
 
 definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)