added lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp

--- a/NEWS	Wed Nov 23 10:27:24 2022 +0100
+++ b/NEWS	Thu Nov 24 10:02:26 2022 +0100
@@ -38,6 +38,8 @@
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
+      asym_if_irrefl_and_trans
+      asymp_if_irreflp_and_transp
       irrefl_onD
       irrefl_onI
       irrefl_on_converse[simp]

--- a/src/HOL/Relation.thy	Wed Nov 23 10:27:24 2022 +0100
+++ b/src/HOL/Relation.thy	Thu Nov 24 10:02:26 2022 +0100
@@ -561,6 +561,12 @@
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
   by (simp add: transp_def)
 
+lemma asym_if_irrefl_and_trans: "irrefl R \<Longrightarrow> trans R \<Longrightarrow> asym R"
+  by (auto intro: asymI dest: transD irreflD)
+
+lemma asymp_if_irreflp_and_transp: "irreflp R \<Longrightarrow> transp R \<Longrightarrow> asymp R"
+  by (rule asym_if_irrefl_and_trans[to_pred])
+
 context preorder
 begin