src/HOL/Library/Extended_Real.thy

--- a/src/HOL/Library/Extended_Real.thy	Thu Aug 21 21:33:34 2025 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Aug 22 16:00:54 2025 +0100
@@ -1096,6 +1096,30 @@
     by (simp add: inc numeral_inc)
 qed
 
+lemma m1_ereal_less_iff [simp]:
+  "((-1::ereal) < numeral a) \<longleftrightarrow> ((-1::real) < numeral a)"
+  by (simp add: one_ereal_def)
+
+lemma m1_ereal_le_iff [simp]:
+  "((-1::ereal) \<le> numeral a) \<longleftrightarrow> ((-1::real) \<le> numeral a)"
+  by (simp add: one_ereal_def)
+
+lemma m1_ereal_eq_iff [simp]:
+  "((-1::ereal) = numeral a) \<longleftrightarrow> ((-1::real) = numeral a)"
+  by (simp add: one_ereal_def)
+
+lemma ereal_less_m1_iff [simp]:
+  "(numeral a < (-1::ereal)) \<longleftrightarrow> (numeral a < (-1::real))"
+  by (simp add: one_ereal_def)
+
+lemma ereal_le_m1_iff [simp]:
+  "(numeral a \<le> (-1::ereal)) \<longleftrightarrow> (numeral a \<le> (-1::real))"
+  by (simp add: one_ereal_def)
+
+lemma ereal_eq_m1_iff [simp]:
+  "(numeral a = (-1::ereal)) \<longleftrightarrow> (numeral a = (-1::real))"
+  by (simp add: one_ereal_def)
+
 lemma distrib_left_ereal_nn:
   "c \<ge> 0 \<Longrightarrow> (x + y) * ereal c = x * ereal c + y * ereal c"
   by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs)