# HG changeset patch
# User noschinl
# Date 1357849331 -3600
# Node ID 5601ae5926791ae16f22cb6a454c939dc0e78185
# Parent  fec14e8fefb82752bee7c1d50856ea9f9308e714
added some ereal_of_enat_* lemmas (from $AFP/thys/Girth_Chromatic)

diff -r fec14e8fefb8 -r 5601ae592679 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jan 10 18:19:13 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jan 10 21:22:11 2013 +0100
@@ -1752,10 +1752,18 @@
   "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
 by (cases m n rule: enat2_cases) auto
 
+lemma ereal_of_enat_less_iff[simp]:
+  "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
+by (cases m n rule: enat2_cases) auto
+
 lemma numeral_le_ereal_of_enat_iff[simp]:
   shows "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
 by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
 
+lemma numeral_less_ereal_of_enat_iff[simp]:
+  shows "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
+by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
+
 lemma ereal_of_enat_ge_zero_cancel_iff[simp]:
   "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
 by (cases n) (auto simp: enat_0[symmetric])
@@ -1768,6 +1776,11 @@
   "ereal_of_enat 0 = 0"
 by (auto simp: enat_0[symmetric])
 
+lemma ereal_of_enat_inf[simp]:
+  "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
+  by (cases n) auto
+
+
 lemma ereal_of_enat_add:
   "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
 by (cases m n rule: enat2_cases) auto