proposition: Lemma nb_surj_nn n: nb_surj n n = n`!.
proof: Proof. elim:n; first by rewrite nb_surj_00. move => n Hrec; rewrite nb_surj_rec - {1} addn1 nb_surj_small addr0 Hrec //. rewrite factS mulnC PoszM pmulrn - mulrzr intz //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)