--- a/src/HOL/Archimedean_Field.thy Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Archimedean_Field.thy Tue Apr 03 14:09:37 2012 +0200
@@ -194,6 +194,9 @@
lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
using floor_of_int [of "of_nat n"] by simp
+lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
+ by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
+
text {* Floor with numerals *}
lemma floor_zero [simp]: "floor 0 = 0"
@@ -340,6 +343,9 @@
lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
using ceiling_of_int [of "of_nat n"] by simp
+lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
+ by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
+
text {* Ceiling with numerals *}
lemma ceiling_zero [simp]: "ceiling 0 = 0"