proposition: Lemma nbsurj_stirling n p: nb_surj n p = nbsurj n p.
proof: Proof. move: n p; elim. case => //; first by rewrite nb_surj_00 nbsurj00. by move => p; rewrite nb_surj_0p nbsurj0n. move => n H [|p]; first by rewrite nb_surj_n0 nbsurjn0. by rewrite nb_surj_rec nbsurjS addnC H H - PoszD mulnC pmulrn mulrzz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)