proposition: Lemma nb_surj_SSnn n: nb_surj n.+2 n = (('C(n.+3,4) + 2 * 'C(n.+2,4)) * n`!) %N.
proof: Proof. elim:n; first by rewrite nb_surj_n0 bin_small //. move => n Hrec; rewrite nb_surj_rec Hrec nb_surj_Snn. rewrite pmulrn - mulrzr intz - PoszD - PoszM mulnDl - mulnA. rewrite 2! (mulnC _ n.+1) - factS mulnA - mulnDl -addnA. rewrite (binS (n.+3)) - addnA;congr( Posz ((_ + _) * _)). rewrite (binS (n.+2) 3) mulnDr addnA (addnC 'C(n.+3, 3)) (binS (n.+2)). rewrite - addnA (addnC _ 'C(n.+2, 2)) -addnA (mulSn n);congr(addn _ (addn _ _)). by rewrite - (addn2 n) (mul_Sm_binm_1 n 2) - {1}(addn2 1) mulnDl mul1n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)