(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Marco B. Caminati * Christoph Lange Dually licenced under * Creative Commons Attribution (CC-BY) 3.0 * ISC License (1-clause BSD License) See LICENSE file for details (Rationale for this dual licence: http://arxiv.org/abs/1107.3212) *) header {* Additional material that we would have expected in Finite_Set.thy *} theory Finite_SetUtils imports Main begin section {* cardinality *} lemma card_diff_gt_0: assumes "finite B" and "card A > card B" shows "card (A - B) > 0" using assms by (metis diff_card_le_card_Diff le_0_eq neq0_conv zero_less_diff) text {* A set of non-zero cardinality is not empty *} lemma card_gt_0_imp_non_empty: fixes A::"'a set" assumes "card A > 0" shows "A \ {}" using assms by fastforce text {* A finite, non-empty set (i.e.\ having a non-zero cardinality) has a member. *} lemma card_gt_0_imp_member: fixes A::"'a set" assumes "card A > 0" obtains y where "y \ A" using assms by fastforce end