proposition: Lemma card_finset (T : finType) (P : pred T) : #|` [fset x in P] | = #|P|.
proof: Proof. by rewrite card_imfset //= -cardE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)