fact: Definition card_impl (E:set A) : nat := mmin le (fun n => exists L, list_covers_impl E L /\ n = length L).
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)