proposition: Lemma card_ge_one : forall A (E:set A) x, x \in E -> finite E -> 1%nat <= card E.
proof: Proof. Proof using. intros. rewrite <- (card_single x). applys~ card_le_of_incl. set_prove. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)