822 lemma fcard_gt_0:

   822 lemma fcard_gt_0:

   823   shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"

   823   shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"

   824   by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)

   824   by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)

   825   

   825   

   826 lemma fcard_not_fin:

   826 lemma fcard_not_fin:

   831 

   829 

   832 lemma fcard_suc: 

   830 lemma fcard_suc: 

   833   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"

   831   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"

   834   apply(descending)

   832   apply(descending)

   835   apply(simp add: fcard_raw_def memb_def)

   833   apply(simp add: fcard_raw_def memb_def)

  1202   shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"

  1200   shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"

  1203   unfolding fcard_set fdelete_set fin_set

  1201   unfolding fcard_set fdelete_set fin_set

  1204   by (rule card_Diff2_less[OF finite_fset])

  1202   by (rule card_Diff2_less[OF finite_fset])

  1205 

  1203 

  1206 lemma fcard_delete1_le: 

  1204 lemma fcard_delete1_le: 

  1208   unfolding fdelete_set fcard_set

  1206   unfolding fdelete_set fcard_set

  1209   by (rule card_Diff1_le[OF finite_fset])

  1207   by (rule card_Diff1_le[OF finite_fset])

  1210 

  1208 

  1211 lemma fcard_psubset: 

  1209 lemma fcard_psubset: 

  1212   shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"

  1210   shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"