diff -r 06e195515deb -r 87429bdecad5 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Real.thy	Mon Jun 30 15:45:21 2014 +0200
@@ -1429,6 +1429,12 @@
   ultimately show ?thesis by fast
 qed
 
+lemma of_rat_dense:
+  fixes x y :: real
+  assumes "x < y"
+  shows "\<exists>q :: rat. x < of_rat q \<and> of_rat q < y"
+using Rats_dense_in_real [OF `x < y`]
+by (auto elim: Rats_cases)
 
 
 subsection{*Numerals and Arithmetic*}
@@ -1444,7 +1450,7 @@
   "real (- numeral v :: int) = - numeral v"
 by (simp_all add: real_of_int_def)
 
-lemma real_of_nat_numeral [simp]:
+lemma  real_of_nat_numeral [simp]:
   "real (numeral v :: nat) = numeral v"
 by (simp add: real_of_nat_def)
 
@@ -1995,9 +2001,15 @@
   unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
   by simp
 
-lemma Rats_unbounded: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
+lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
   by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
 
+lemma Rats_no_bot_less: "\<exists> q \<in> \<rat>. q < (x :: real)"
+  apply (auto intro!: bexI[of _ "of_int (floor x - 1)"])
+  apply (rule less_le_trans[OF _ of_int_floor_le])
+  apply simp
+  done
+
 subsection {* Exponentiation with floor *}
 
 lemma floor_power: