proposition: Lemma card_partition_aux (T:finType) (P: {set {set T}}) E: partition P E -> #|P| <= #|E|.
proof: Proof. move => pe;rewrite (card_partition pe) - sum1_card; apply: leq_sum => i. rewrite card_gt0; apply: (partition_ni_set0 pe). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)