proposition: Lemma card_set_pred: forall (T:finType) (P:T -> bool), #|[set f:T | P f]| = #|[pred f:T | P f]|.
proof: Proof. by move => T P; apply: eq_card; move => t; rewrite in_set. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)