# HG changeset patch
# User hoelzl
# Date 1414408884 -3600
# Node ID 387f65e69dd5c9d0ffa5543a38006a1398744228
# Parent  d17b3844b72679215d88970c0bdcdc37ac235753
further generalization of natfloor_div_nat

diff -r d17b3844b726 -r 387f65e69dd5 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Oct 27 12:03:13 2014 +0100
+++ b/src/HOL/Real.thy	Mon Oct 27 12:21:24 2014 +0100
@@ -1913,9 +1913,12 @@
     "natfloor(x - real a) = natfloor x - a"
   by linarith
 
-lemma natfloor_div_nat: "0 \<le> x \<Longrightarrow> natfloor (x / real y) = natfloor x div y"
-  unfolding natfloor_def real_of_int_of_nat_eq[symmetric]
-  by (subst floor_divide_real_eq_div) (simp_all add: nat_div_distrib)
+lemma natfloor_div_nat: "natfloor (x / real y) = natfloor x div y"
+proof cases
+  assume "0 \<le> x" then show ?thesis
+    unfolding natfloor_def real_of_int_of_nat_eq[symmetric]
+    by (subst floor_divide_real_eq_div) (simp_all add: nat_div_distrib)
+qed (simp add: divide_nonpos_nonneg natfloor_neg)
 
 lemma natfloor_div_numeral[simp]:
   "natfloor (numeral x / numeral y) = numeral x div numeral y"