proposition: Lemma Bell_pr2 E: finite_set E -> cardinal (partitions E) = Bell_number (cardinal E).
proof: Proof. move => fse; move/NatP: (fse) => nN. rewrite (Bell_pr fse) (Bell_pr1 nN). by apply: csumb_exten => p pn; rewrite nbpart_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)