proposition: Lemma nb_surj_Snn n: nb_surj n.+1 n = ('C(n.+1,2) * n`!) %N.
proof: Proof. elim:n; first by rewrite nb_surj_n0 bin_small //. move => n Hrec; rewrite nb_surj_rec Hrec nb_surj_nn. rewrite pmulrn - mulrzr intz - PoszD - PoszM (binS (n.+1)) bin1 mulnDl. by rewrite - mulnA 2! (mulnC _ n.+1) - factS - mulnDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)