proposition: Lemma nb_surj_rec n p: nb_surj n.+1 p.+1 = (nb_surj n p + nb_surj n p.+1) *+ (p.+1).
proof: Proof. set f: (nat -> int ):= (fun i : nat => (i ^ n)%N). rewrite (bin_conv_inv_rec (f:=f)) // /bin_conv_inv -mulrnAr - sumrMnl. rewrite /nb_surj /bin_conv_inv /=. have ->: (\sum_(i < p.+1) (-1) ^+ i * f i.+1 *+ 'C(p, i) *+ p.+1) = (\sum_(i < p.+1) (-1) ^+ i * ((i.+1) ^(n.+1))%N%:Z *+ 'C(p.+1, i.+1)). apply:eq_bigr => i /= _; rewrite /f expnS mulnC PoszM mulrA - mulrnA. rewrite mulnC mul_bin_diag mulrnA; congr ( _ *+ _). by rewrite pmulrn - mulrzr intz. rewrite exprSr - mulrA big_distrr /= big_ord_recl /= exp0n //(_: Posz 0 = 0) //. rewrite mulr0 add0r; congr ( _ * _); apply: eq_bigr => i _ /=. by rewrite mulrnAr mulrA exprS mulN1r mulN1r opprK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)