diff -r 0acfdb151e52 -r 0ddb5b755cdc src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/Real.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -1319,7 +1319,6 @@
 lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
 by (simp add: real_eq_of_nat)
 
-
 lemma Rats_eq_int_div_int:
   "\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
 proof
@@ -1996,6 +1995,9 @@
   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"
+  by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
+
 subsection {* Exponentiation with floor *}
 
 lemma floor_power: