proposition: Lemma Bell_pr1 n: natp n -> Bell_number n = csumb (Nintc n) (nbpart n).
proof: Proof. move => nN. by rewrite /Bell_number (Bell_pr (finite_Nint n)) /nbpart (card_Nint nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)