# HG changeset patch
# User huffman
# Date 1315144570 25200
# Node ID 37ce74ff42034d9fb32c7902bffa2598e017cb23
# Parent  487ae6317f7bca261a4e0c5bbb0e04344d665c4b
remove unused assumptions from natceiling lemmas

diff -r 487ae6317f7b -r 37ce74ff4203 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Sun Sep 04 06:27:59 2011 -0700
+++ b/src/HOL/RComplete.thy	Sun Sep 04 06:56:10 2011 -0700
@@ -475,12 +475,12 @@
   unfolding natceiling_def real_of_nat_def
   by (simp add: nat_le_iff ceiling_le_iff)
 
-lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
-  unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *)
+lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
+  unfolding natceiling_def real_of_nat_def
   by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_le_eq_number_of [simp]:
-    "~ neg((number_of n)::int) ==> 0 <= x ==>
+    "~ neg((number_of n)::int) ==>
       (natceiling x <= number_of n) = (x <= number_of n)"
   by (simp add: natceiling_le_eq)