proposition: Lemma nbpart_pr E p: finite_set E -> cardinal (partitionsx E p) = nbpart (cardinal E) p.
proof: Proof. move => fse; set n := (cardinal E). have : n = cardinal (Nint n) by rewrite card_Nint //; apply /NatP. move/card_eqP => [g gp]; apply /card_eqP. exists (Lf (extension_p3 g) (partitionsx E p) (partitionsx (Nint n) p)). hnf; saw; apply: (nbpart_pr1 p gp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)