src/HOL/Library/Infinite_Set.thy

--- a/src/HOL/Library/Infinite_Set.thy	Wed Jul 27 13:17:32 2022 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Jul 28 12:33:20 2022 +0100
@@ -267,6 +267,10 @@
   "infinite S \<Longrightarrow> enumerate S m < enumerate S n \<longleftrightarrow> m < n"
   by (metis enumerate_mono less_asym less_linear)
 
+lemma enumerate_mono_le_iff [simp]:
+  "infinite S \<Longrightarrow> enumerate S m \<le> enumerate S n \<longleftrightarrow> m \<le> n"
+  by (meson enumerate_mono_iff not_le)
+
 lemma le_enumerate:
   assumes S: "infinite S"
   shows "n \<le> enumerate S n"