--- 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: