fact: Definition Pcard_subset n P P' : P [<=] P' -> Pcard P n -> Pcard P' n.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)