tuned lemma

--- a/src/HOL/Finite_Set.thy	Wed Mar 16 19:50:56 2011 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 17 09:58:13 2011 +0100
@@ -1932,7 +1932,7 @@
 lemma card_Collect_less_nat[simp]: "card{i::nat. i < n} = n"
 by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)
 
-lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = n+1"
+lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = Suc n"
 using card_Collect_less_nat[of "Suc n"] by(simp add: less_Suc_eq_le)
 
 lemma card_mono: