--- 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)