--- a/src/HOL/RComplete.thy Sun Sep 04 14:29:15 2011 +0200
+++ b/src/HOL/RComplete.thy Sun Sep 04 06:27:59 2011 -0700
@@ -336,9 +336,6 @@
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
unfolding natfloor_def by simp
-lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
- by simp (* TODO: move to Int.thy *)
-
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
unfolding natfloor_def by (intro nat_mono floor_mono)
@@ -474,9 +471,6 @@
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
unfolding natceiling_def by (intro nat_mono ceiling_mono)
-lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
- by auto (* TODO: move to Int.thy *)
-
lemma natceiling_le: "x <= real a ==> natceiling x <= a"
unfolding natceiling_def real_of_nat_def
by (simp add: nat_le_iff ceiling_le_iff)