src/HOL/Real.thy
changeset 58040 9a867afaab5a
parent 57514 bdc2c6b40bf2
child 58042 ffa9e39763e3
     1.1 --- a/src/HOL/Real.thy	Mon Aug 25 09:40:50 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Tue Aug 19 18:37:32 2014 +0200
     1.3 @@ -1463,12 +1463,14 @@
     1.4        @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
     1.5        @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
     1.6        @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
     1.7 -      @{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}]
     1.8 +      @{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)},
     1.9 +      @{thm real_of_int_def[symmetric]}, @{thm real_of_nat_def[symmetric]}]
    1.10    #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat \<Rightarrow> real"})
    1.11 -  #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"}))
    1.12 +  #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"})
    1.13 +  #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \<Rightarrow> real"})
    1.14 +  #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"}))
    1.15  *}
    1.16  
    1.17 -
    1.18  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
    1.19  
    1.20  lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" 
    1.21 @@ -1650,78 +1652,66 @@
    1.22  lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)"
    1.23  unfolding real_of_int_def by (rule floor_exists)
    1.24  
    1.25 -lemma lemma_floor:
    1.26 -  assumes a1: "real m \<le> r" and a2: "r < real n + 1"
    1.27 -  shows "m \<le> (n::int)"
    1.28 -proof -
    1.29 -  have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans)
    1.30 -  also have "... = real (n + 1)" by simp
    1.31 -  finally have "m < n + 1" by (simp only: real_of_int_less_iff)
    1.32 -  thus ?thesis by arith
    1.33 -qed
    1.34 +lemma lemma_floor: "real m \<le> r \<Longrightarrow> r < real n + 1 \<Longrightarrow> m \<le> (n::int)"
    1.35 +  by simp
    1.36  
    1.37  lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r"
    1.38  unfolding real_of_int_def by (rule of_int_floor_le)
    1.39  
    1.40  lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x"
    1.41 -by (auto intro: lemma_floor)
    1.42 +  by simp
    1.43  
    1.44  lemma real_of_int_floor_cancel [simp]:
    1.45      "(real (floor x) = x) = (\<exists>n::int. x = real n)"
    1.46    using floor_real_of_int by metis
    1.47  
    1.48  lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
    1.49 -  unfolding real_of_int_def using floor_unique [of n x] by simp
    1.50 +  by linarith
    1.51  
    1.52  lemma floor_eq2: "[| real n \<le> x; x < real n + 1 |] ==> floor x = n"
    1.53 -  unfolding real_of_int_def by (rule floor_unique)
    1.54 +  by linarith
    1.55  
    1.56  lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
    1.57 -apply (rule inj_int [THEN injD])
    1.58 -apply (simp add: real_of_nat_Suc)
    1.59 -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
    1.60 -done
    1.61 +  by linarith
    1.62  
    1.63  lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
    1.64 -apply (drule order_le_imp_less_or_eq)
    1.65 -apply (auto intro: floor_eq3)
    1.66 -done
    1.67 +  by linarith
    1.68  
    1.69  lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)"
    1.70 -  unfolding real_of_int_def using floor_correct [of r] by simp
    1.71 +  by linarith
    1.72  
    1.73  lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
    1.74 -  unfolding real_of_int_def using floor_correct [of r] by simp
    1.75 +  by linarith
    1.76  
    1.77  lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"
    1.78 -  unfolding real_of_int_def using floor_correct [of r] by simp
    1.79 +  by linarith
    1.80  
    1.81  lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1"
    1.82 -  unfolding real_of_int_def using floor_correct [of r] by simp
    1.83 +  by linarith
    1.84  
    1.85  lemma le_floor: "real a <= x ==> a <= floor x"
    1.86 -  unfolding real_of_int_def by (simp add: le_floor_iff)
    1.87 +  by linarith
    1.88  
    1.89  lemma real_le_floor: "a <= floor x ==> real a <= x"
    1.90 -  unfolding real_of_int_def by (simp add: le_floor_iff)
    1.91 +  by linarith
    1.92  
    1.93  lemma le_floor_eq: "(a <= floor x) = (real a <= x)"
    1.94 -  unfolding real_of_int_def by (rule le_floor_iff)
    1.95 +  by linarith
    1.96  
    1.97  lemma floor_less_eq: "(floor x < a) = (x < real a)"
    1.98 -  unfolding real_of_int_def by (rule floor_less_iff)
    1.99 +  by linarith
   1.100  
   1.101  lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)"
   1.102 -  unfolding real_of_int_def by (rule less_floor_iff)
   1.103 +  by linarith
   1.104  
   1.105  lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)"
   1.106 -  unfolding real_of_int_def by (rule floor_le_iff)
   1.107 +  by linarith
   1.108  
   1.109  lemma floor_add [simp]: "floor (x + real a) = floor x + a"
   1.110 -  unfolding real_of_int_def by (rule floor_add_of_int)
   1.111 +  by linarith
   1.112  
   1.113  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
   1.114 -  unfolding real_of_int_def by (rule floor_diff_of_int)
   1.115 +  by linarith
   1.116  
   1.117  lemma le_mult_floor:
   1.118    assumes "0 \<le> (a :: real)" and "0 \<le> b"
   1.119 @@ -1746,56 +1736,56 @@
   1.120  qed (auto simp: real_of_int_div)
   1.121  
   1.122  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   1.123 -  unfolding real_of_nat_def by simp
   1.124 +  by linarith
   1.125  
   1.126  lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   1.127 -  unfolding real_of_int_def by (rule le_of_int_ceiling)
   1.128 +  by linarith
   1.129  
   1.130  lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n"
   1.131 -  unfolding real_of_int_def by simp
   1.132 +  by linarith
   1.133  
   1.134  lemma real_of_int_ceiling_cancel [simp]:
   1.135       "(real (ceiling x) = x) = (\<exists>n::int. x = real n)"
   1.136    using ceiling_real_of_int by metis
   1.137  
   1.138  lemma ceiling_eq: "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1"
   1.139 -  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   1.140 +  by linarith
   1.141  
   1.142  lemma ceiling_eq2: "[| real n < x; x \<le> real n + 1 |] ==> ceiling x = n + 1"
   1.143 -  unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp
   1.144 +  by linarith
   1.145  
   1.146  lemma ceiling_eq3: "[| real n - 1 < x; x \<le> real n  |] ==> ceiling x = n"
   1.147 -  unfolding real_of_int_def using ceiling_unique [of n x] by simp
   1.148 +  by linarith
   1.149  
   1.150  lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r) - 1 \<le> r"
   1.151 -  unfolding real_of_int_def using ceiling_correct [of r] by simp
   1.152 +  by linarith
   1.153  
   1.154  lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1"
   1.155 -  unfolding real_of_int_def using ceiling_correct [of r] by simp
   1.156 +  by linarith
   1.157  
   1.158  lemma ceiling_le: "x <= real a ==> ceiling x <= a"
   1.159 -  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   1.160 +  by linarith
   1.161  
   1.162  lemma ceiling_le_real: "ceiling x <= a ==> x <= real a"
   1.163 -  unfolding real_of_int_def by (simp add: ceiling_le_iff)
   1.164 +  by linarith
   1.165  
   1.166  lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)"
   1.167 -  unfolding real_of_int_def by (rule ceiling_le_iff)
   1.168 +  by linarith
   1.169  
   1.170  lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)"
   1.171 -  unfolding real_of_int_def by (rule less_ceiling_iff)
   1.172 +  by linarith
   1.173  
   1.174  lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a - 1)"
   1.175 -  unfolding real_of_int_def by (rule ceiling_less_iff)
   1.176 +  by linarith
   1.177  
   1.178  lemma le_ceiling_eq: "(a <= ceiling x) = (real a - 1 < x)"
   1.179 -  unfolding real_of_int_def by (rule le_ceiling_iff)
   1.180 +  by linarith
   1.181  
   1.182  lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a"
   1.183 -  unfolding real_of_int_def by (rule ceiling_add_of_int)
   1.184 +  by linarith
   1.185  
   1.186  lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   1.187 -  unfolding real_of_int_def by (rule ceiling_diff_of_int)
   1.188 +  by linarith
   1.189  
   1.190  
   1.191  subsubsection {* Versions for the natural numbers *}
   1.192 @@ -1808,111 +1798,88 @@
   1.193    natceiling :: "real => nat" where
   1.194    "natceiling x = nat(ceiling x)"
   1.195  
   1.196 +lemma natfloor_split[arith_split]: "P (natfloor t) \<longleftrightarrow> (t < 0 \<longrightarrow> P 0) \<and> (\<forall>n. of_nat n \<le> t \<and> t < of_nat n + 1 \<longrightarrow> P n)"
   1.197 +proof -
   1.198 +  have [dest]: "\<And>n m::nat. real n \<le> t \<Longrightarrow> t < real n + 1 \<Longrightarrow> real m \<le> t \<Longrightarrow> t < real m + 1 \<Longrightarrow> n = m"
   1.199 +    by simp
   1.200 +  show ?thesis
   1.201 +    by (auto simp: natfloor_def real_of_nat_def[symmetric] split: split_nat floor_split)
   1.202 +qed
   1.203 +
   1.204 +lemma natceiling_split[arith_split]:
   1.205 +  "P (natceiling t) \<longleftrightarrow> (t \<le> - 1 \<longrightarrow> P 0) \<and> (\<forall>n. of_nat n - 1 < t \<and> t \<le> of_nat n \<longrightarrow> P n)"
   1.206 +proof -
   1.207 +  have [dest]: "\<And>n m::nat. real n - 1 < t \<Longrightarrow> t \<le> real n \<Longrightarrow> real m - 1 < t \<Longrightarrow> t \<le> real m \<Longrightarrow> n = m"
   1.208 +    by simp
   1.209 +  show ?thesis
   1.210 +    by (auto simp: natceiling_def real_of_nat_def[symmetric] split: split_nat ceiling_split)
   1.211 +qed
   1.212 +
   1.213  lemma natfloor_zero [simp]: "natfloor 0 = 0"
   1.214 -  by (unfold natfloor_def, simp)
   1.215 +  by linarith
   1.216  
   1.217  lemma natfloor_one [simp]: "natfloor 1 = 1"
   1.218 -  by (unfold natfloor_def, simp)
   1.219 -
   1.220 -lemma zero_le_natfloor [simp]: "0 <= natfloor x"
   1.221 -  by (unfold natfloor_def, simp)
   1.222 +  by linarith
   1.223  
   1.224  lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
   1.225    by (unfold natfloor_def, simp)
   1.226  
   1.227  lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
   1.228 -  by (unfold natfloor_def, simp)
   1.229 +  by linarith
   1.230  
   1.231  lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
   1.232 -  by (unfold natfloor_def, simp)
   1.233 +  by linarith
   1.234  
   1.235  lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
   1.236 -  unfolding natfloor_def by simp
   1.237 +  by linarith
   1.238  
   1.239  lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   1.240 -  unfolding natfloor_def by (intro nat_mono floor_mono)
   1.241 +  by linarith
   1.242  
   1.243  lemma le_natfloor: "real x <= a ==> x <= natfloor a"
   1.244 -  apply (unfold natfloor_def)
   1.245 -  apply (subst nat_int [THEN sym])
   1.246 -  apply (rule nat_mono)
   1.247 -  apply (rule le_floor)
   1.248 -  apply simp
   1.249 -done
   1.250 +  by linarith
   1.251  
   1.252  lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
   1.253 -  unfolding natfloor_def real_of_nat_def
   1.254 -  by (simp add: nat_less_iff floor_less_iff)
   1.255 +  by linarith
   1.256  
   1.257 -lemma less_natfloor:
   1.258 -  assumes "0 \<le> x" and "x < real (n :: nat)"
   1.259 -  shows "natfloor x < n"
   1.260 -  using assms by (simp add: natfloor_less_iff)
   1.261 +lemma less_natfloor: "0 \<le> x \<Longrightarrow> x < real (n :: nat) \<Longrightarrow> natfloor x < n"
   1.262 +  by linarith
   1.263  
   1.264  lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   1.265 -  apply (rule iffI)
   1.266 -  apply (rule order_trans)
   1.267 -  prefer 2
   1.268 -  apply (erule real_natfloor_le)
   1.269 -  apply (subst real_of_nat_le_iff)
   1.270 -  apply assumption
   1.271 -  apply (erule le_natfloor)
   1.272 -done
   1.273 +  by linarith
   1.274  
   1.275  lemma le_natfloor_eq_numeral [simp]:
   1.276 -    "~ neg((numeral n)::int) ==> 0 <= x ==>
   1.277 -      (numeral n <= natfloor x) = (numeral n <= x)"
   1.278 -  apply (subst le_natfloor_eq, assumption)
   1.279 -  apply simp
   1.280 -done
   1.281 +    "0 \<le> x \<Longrightarrow> (numeral n \<le> natfloor x) = (numeral n \<le> x)"
   1.282 +  by (subst le_natfloor_eq, assumption) simp
   1.283 +
   1.284 +lemma le_natfloor_eq_one [simp]: "(1 \<le> natfloor x) = (1 \<le> x)"
   1.285 +  by linarith
   1.286  
   1.287 -lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
   1.288 -  apply (case_tac "0 <= x")
   1.289 -  apply (subst le_natfloor_eq, assumption, simp)
   1.290 -  apply (rule iffI)
   1.291 -  apply (subgoal_tac "natfloor x <= natfloor 0")
   1.292 -  apply simp
   1.293 -  apply (rule natfloor_mono)
   1.294 -  apply simp
   1.295 -  apply simp
   1.296 -done
   1.297 +lemma natfloor_eq: "real n \<le> x \<Longrightarrow> x < real n + 1 \<Longrightarrow> natfloor x = n"
   1.298 +  by linarith
   1.299  
   1.300 -lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
   1.301 -  unfolding natfloor_def by (simp add: floor_eq2 [where n="int n"])
   1.302 -
   1.303 -lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1"
   1.304 -  apply (case_tac "0 <= x")
   1.305 -  apply (unfold natfloor_def)
   1.306 -  apply simp
   1.307 -  apply simp_all
   1.308 -done
   1.309 +lemma real_natfloor_add_one_gt: "x < real (natfloor x) + 1"
   1.310 +  by linarith
   1.311  
   1.312  lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
   1.313 -using real_natfloor_add_one_gt by (simp add: algebra_simps)
   1.314 +  by linarith
   1.315  
   1.316  lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
   1.317 -  apply (subgoal_tac "z < real(natfloor z) + 1")
   1.318 -  apply arith
   1.319 -  apply (rule real_natfloor_add_one_gt)
   1.320 -done
   1.321 +  by linarith
   1.322  
   1.323  lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
   1.324 -  unfolding natfloor_def
   1.325 -  unfolding real_of_int_of_nat_eq [symmetric] floor_add
   1.326 -  by (simp add: nat_add_distrib)
   1.327 +  by linarith
   1.328  
   1.329  lemma natfloor_add_numeral [simp]:
   1.330 -    "~neg ((numeral n)::int) ==> 0 <= x ==>
   1.331 -      natfloor (x + numeral n) = natfloor x + numeral n"
   1.332 +    "0 <= x \<Longrightarrow> natfloor (x + numeral n) = natfloor x + numeral n"
   1.333    by (simp add: natfloor_add [symmetric])
   1.334  
   1.335  lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
   1.336 -  by (simp add: natfloor_add [symmetric] del: One_nat_def)
   1.337 +  by linarith
   1.338  
   1.339  lemma natfloor_subtract [simp]:
   1.340      "natfloor(x - real a) = natfloor x - a"
   1.341 -  unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
   1.342 -  by simp
   1.343 +  by linarith
   1.344  
   1.345  lemma natfloor_div_nat:
   1.346    assumes "1 <= x" and "y > 0"
   1.347 @@ -1939,67 +1906,57 @@
   1.348      (auto simp add: le_natfloor_eq mult_mono' real_natfloor_le natfloor_neg)
   1.349  
   1.350  lemma natceiling_zero [simp]: "natceiling 0 = 0"
   1.351 -  by (unfold natceiling_def, simp)
   1.352 +  by linarith
   1.353  
   1.354  lemma natceiling_one [simp]: "natceiling 1 = 1"
   1.355 -  by (unfold natceiling_def, simp)
   1.356 +  by linarith
   1.357  
   1.358  lemma zero_le_natceiling [simp]: "0 <= natceiling x"
   1.359 -  by (unfold natceiling_def, simp)
   1.360 +  by linarith
   1.361  
   1.362  lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
   1.363 -  by (unfold natceiling_def, simp)
   1.364 +  by (simp add: natceiling_def)
   1.365  
   1.366  lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
   1.367 -  by (unfold natceiling_def, simp)
   1.368 +  by linarith
   1.369  
   1.370  lemma real_natceiling_ge: "x <= real(natceiling x)"
   1.371 -  unfolding natceiling_def by (cases "x < 0", simp_all)
   1.372 +  by linarith
   1.373  
   1.374  lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
   1.375 -  unfolding natceiling_def by simp
   1.376 +  by linarith
   1.377  
   1.378  lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   1.379 -  unfolding natceiling_def by (intro nat_mono ceiling_mono)
   1.380 +  by linarith
   1.381  
   1.382  lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   1.383 -  unfolding natceiling_def real_of_nat_def
   1.384 -  by (simp add: nat_le_iff ceiling_le_iff)
   1.385 +  by linarith
   1.386  
   1.387  lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
   1.388 -  unfolding natceiling_def real_of_nat_def
   1.389 -  by (simp add: nat_le_iff ceiling_le_iff)
   1.390 +  by linarith
   1.391  
   1.392  lemma natceiling_le_eq_numeral [simp]:
   1.393 -    "~ neg((numeral n)::int) ==>
   1.394 -      (natceiling x <= numeral n) = (x <= numeral n)"
   1.395 +    "(natceiling x <= numeral n) = (x <= numeral n)"
   1.396    by (simp add: natceiling_le_eq)
   1.397  
   1.398  lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
   1.399 -  unfolding natceiling_def
   1.400 -  by (simp add: nat_le_iff ceiling_le_iff)
   1.401 +  by linarith
   1.402  
   1.403  lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
   1.404 -  unfolding natceiling_def
   1.405 -  by (simp add: ceiling_eq2 [where n="int n"])
   1.406 +  by linarith
   1.407  
   1.408 -lemma natceiling_add [simp]: "0 <= x ==>
   1.409 -    natceiling (x + real a) = natceiling x + a"
   1.410 -  unfolding natceiling_def
   1.411 -  unfolding real_of_int_of_nat_eq [symmetric] ceiling_add
   1.412 -  by (simp add: nat_add_distrib)
   1.413 +lemma natceiling_add [simp]: "0 <= x ==> natceiling (x + real a) = natceiling x + a"
   1.414 +  by linarith
   1.415  
   1.416  lemma natceiling_add_numeral [simp]:
   1.417 -    "~ neg ((numeral n)::int) ==> 0 <= x ==>
   1.418 -      natceiling (x + numeral n) = natceiling x + numeral n"
   1.419 +    "0 <= x ==> natceiling (x + numeral n) = natceiling x + numeral n"
   1.420    by (simp add: natceiling_add [symmetric])
   1.421  
   1.422  lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
   1.423 -  by (simp add: natceiling_add [symmetric] del: One_nat_def)
   1.424 +  by linarith
   1.425  
   1.426  lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
   1.427 -  unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
   1.428 -  by simp
   1.429 +  by linarith
   1.430  
   1.431  lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
   1.432    by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)