src/HOL/Real.thy
changeset 56889 48a745e1bde7
parent 56571 f4635657d66f
child 57275 0ddb5b755cdc
     1.1 --- a/src/HOL/Real.thy	Tue May 06 23:35:24 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Wed May 07 12:25:35 2014 +0200
     1.3 @@ -1555,6 +1555,7 @@
     1.4    "real a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
     1.5    unfolding real_of_int_le_iff[symmetric] by simp
     1.6  
     1.7 +
     1.8  subsection{*Density of the Reals*}
     1.9  
    1.10  lemma real_lbound_gt_zero:
    1.11 @@ -1613,6 +1614,14 @@
    1.12  apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
    1.13  done
    1.14  
    1.15 +lemma real_of_nat_less_numeral_iff [simp]:
    1.16 +  "real (n::nat) < numeral w \<longleftrightarrow> n < numeral w"
    1.17 +  using real_of_nat_less_iff[of n "numeral w"] by simp
    1.18 +
    1.19 +lemma numeral_less_real_of_nat_iff [simp]:
    1.20 +  "numeral w < real (n::nat) \<longleftrightarrow> numeral w < n"
    1.21 +  using real_of_nat_less_iff[of "numeral w" n] by simp
    1.22 +
    1.23  lemma numeral_le_real_of_int_iff [simp]:
    1.24       "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
    1.25  by (simp add: linorder_not_less [symmetric])