--- a/src/HOL/Real.thy Tue May 06 23:35:24 2014 +0200
+++ b/src/HOL/Real.thy Wed May 07 12:25:35 2014 +0200
@@ -1555,6 +1555,7 @@
"real a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
unfolding real_of_int_le_iff[symmetric] by simp
+
subsection{*Density of the Reals*}
lemma real_lbound_gt_zero:
@@ -1613,6 +1614,14 @@
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
done
+lemma real_of_nat_less_numeral_iff [simp]:
+ "real (n::nat) < numeral w \<longleftrightarrow> n < numeral w"
+ using real_of_nat_less_iff[of n "numeral w"] by simp
+
+lemma numeral_less_real_of_nat_iff [simp]:
+ "numeral w < real (n::nat) \<longleftrightarrow> numeral w < n"
+ using real_of_nat_less_iff[of "numeral w" n] by simp
+
lemma numeral_le_real_of_int_iff [simp]:
"((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
by (simp add: linorder_not_less [symmetric])