src/HOL/Real/RComplete.thy
changeset 25162 ad4d5365d9d8
parent 25140 273772abbea2
child 27435 b3f8e9bdf9a7
--- a/src/HOL/Real/RComplete.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Real/RComplete.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -1208,10 +1208,10 @@
   apply simp
 done
 
-lemma natfloor_div_nat: "1 <= x ==> y \<noteq> 0 ==>
+lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
   natfloor (x / real y) = natfloor x div y"
 proof -
-  assume "1 <= (x::real)" and "(y::nat) \<noteq> 0"
+  assume "1 <= (x::real)" and "(y::nat) > 0"
   have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
     by simp
   then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +