proposition: Lemma card_partition P D : partition P D -> #|D| = \sum_(A in P) #|A|.
proof: Proof. by case/and3P=> /eqP <- /eqnP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)