src/HOL/Real/RComplete.thy

       (number_of n <= natfloor x) = (number_of n <= x)"
   apply (subst le_natfloor_eq, assumption)
   apply simp
 done
 
-lemma le_natfloor_one_eq [simp]: "(1 <= natfloor x) = (1 <= x)"
+lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
   apply (case_tac "0 <= x")
   apply (subst le_natfloor_eq, assumption, simp)
   apply (rule iffI)
   apply (subgoal_tac "natfloor x <= natfloor 0") 
   apply simp

   apply (subst real_of_nat_le_iff)
   apply assumption
   apply (erule natceiling_le)
 done
 
-lemma natceiling_le_eq2 [simp]: "~ neg((number_of n)::int) ==> 0 <= x ==>
-    (natceiling x <= number_of n) = (x <= number_of n)"
+lemma natceiling_le_eq_number_of [simp]: 
+    "~ neg((number_of n)::int) ==> 0 <= x ==>
+      (natceiling x <= number_of n) = (x <= number_of n)"
   apply (subst natceiling_le_eq, assumption)
   apply simp
 done
 
-lemma natceiling_one_le_eq: "(natceiling x <= 1) = (x <= 1)"
+lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
   apply (case_tac "0 <= x")
   apply (subst natceiling_le_eq)
   apply assumption
   apply simp
   apply (subst natceiling_neg)

   apply (erule ssubst)
   apply (erule ceiling_mono2)
   apply simp_all
 done
 
-lemma natceiling_add2 [simp]: "~ neg ((number_of n)::int) ==> 0 <= x ==> 
-    natceiling (x + number_of n) = natceiling x + number_of n"
+lemma natceiling_add_number_of [simp]: 
+    "~ neg ((number_of n)::int) ==> 0 <= x ==> 
+      natceiling (x + number_of n) = natceiling x + number_of n"
   apply (subst natceiling_add [THEN sym])
   apply simp_all
 done
 
 lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"