fact: Definition finite_inv_card_ge : forall (E:set A) n, finite E -> (forall L, list_covers E L -> (length L >= n)%nat) -> (card E >= n)%nat.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)