# HG changeset patch
# User nipkow
# Date 1470406933 -7200
# Node ID ae810a755cd2793cb4f70c69ff863daa5aa13b37
# Parent  d0fa16751d149a72ba2bedcd2ea136b1ece07197
added missing lemmas

diff -r d0fa16751d14 -r ae810a755cd2 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Fri Aug 05 15:44:53 2016 +0200
+++ b/src/HOL/Real.thy	Fri Aug 05 16:22:13 2016 +0200
@@ -1535,6 +1535,15 @@
   with b show ?thesis by (auto split: floor_split simp: field_simps)
 qed
 
+lemma floor_one_divide_eq_div_numeral [simp]:
+  "\<lfloor>1 / numeral b::real\<rfloor> = 1 div numeral b"
+by (metis floor_divide_of_int_eq of_int_1 of_int_numeral)
+
+lemma floor_minus_one_divide_eq_div_numeral [simp]:
+  "\<lfloor>- (1 / numeral b)::real\<rfloor> = - 1 div numeral b"
+by (metis (mono_tags, hide_lams) div_minus_right minus_divide_right
+    floor_divide_of_int_eq of_int_neg_numeral of_int_1)
+
 lemma floor_divide_eq_div_numeral [simp]:
   "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
 by (metis floor_divide_of_int_eq of_int_numeral)