--- a/src/HOL/Archimedean_Field.thy Mon Sep 26 16:57:05 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy Tue Sep 27 16:24:53 2016 +0100
@@ -619,6 +619,15 @@
unfolding ceiling_def by simp
+subsection \<open>Natural numbers\<close>
+
+lemma of_nat_floor: "r\<ge>0 \<Longrightarrow> of_nat (nat \<lfloor>r\<rfloor>) \<le> r"
+ by simp
+
+lemma of_nat_ceiling: "of_nat (nat \<lceil>r\<rceil>) \<ge> r"
+ by (cases "r\<ge>0") auto
+
+
subsection \<open>Frac Function\<close>
definition frac :: "'a \<Rightarrow> 'a::floor_ceiling"