1.1 --- a/src/HOL/RComplete.thy	Wed Apr 18 14:29:18 2012 +0200
     1.2 +++ b/src/HOL/RComplete.thy	Wed Apr 18 14:29:19 2012 +0200
     1.3 @@ -252,6 +252,16 @@
     1.4    finally show ?thesis unfolding real_of_int_less_iff by simp
     1.5  qed
     1.6  
     1.7 +lemma floor_divide_eq_div:
     1.8 +  "floor (real a / real b) = a div b"
     1.9 +proof cases
    1.10 +  assume "b \<noteq> 0 \<or> b dvd a"
    1.11 +  with real_of_int_div3[of a b] show ?thesis
    1.12 +    by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans)
    1.13 +       (metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject
    1.14 +              real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
    1.15 +qed (auto simp: real_of_int_div)
    1.16 +
    1.17  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
    1.18    unfolding real_of_nat_def by simp
    1.19