src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -1250,6 +1250,10 @@
   "card A = 0 \<longleftrightarrow> A = {} \<or> \<not> finite A"
   by auto
 
+lemma card_range_greater_zero:
+  "finite (range f) \<Longrightarrow> card (range f) > 0"
+  by (rule ccontr) (simp add: card_eq_0_iff)
+
 lemma card_gt_0_iff:
   "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
   by (simp add: neq0_conv [symmetric] card_eq_0_iff)