proposition: Lemma Bell_rec n: Bell n.+1 = \sum_(k<n.+1) 'C(n,k) * Bell k.
proof: Proof. suff aux: forall m p, \sum_(k<m.+1) 'C(m,k) * 'St(k,p) = 'St(m.+1,p.+1). transitivity (\sum_(i < n.+1) \sum_(k < n.+1) 'C(n, k) * 'St(k, i)). by rewrite /Bell big_ord_recl add0n; apply: eq_bigr =>i _; rewrite aux. rewrite exchange_big /=; apply: eq_bigr; move=> [i lin ] _. rewrite - big_distrr /= -(subnK lin) (addnC _ i.+1) big_split_ord /=. by rewrite [X in (_ + X)] big1 ? addn0// => j _;rewrite stir_small1 ?leq_addr. Abort. Lemma sum_nbsurj n k: \sum_(i<k.+1) 'Sj(k,i) * 'C(n,i) = n ^k. Proof. move:n; elim:k; first by move => n; rewrite big_ord_recr big_ord0 nbsurj00 bin0. move => k Hrec n; case:n. rewrite expnS mul0n big1 //= => [] [i _] _ /=; case i => //. by move => n; have ->: 'C(0, n.+1) = 0 by []; rewrite muln0. move => n; rewrite expnS - Hrec big_ord_recl nbsurjn0 mul0n add0n. transitivity (n.+1 * \sum_(i < k.+1) (('Sj(k, i) + 'Sj(k, i.+1)) * 'C(n, i))). rewrite big_distrr; apply: eq_bigr; move => [i lik] _ //=. by rewrite nbsurjS addnC mulnAC - mul_bin_diag - mulnA (mulnC _ 'C(n, i)). have aux: 'Sj(k, k.+1) = 0 by rewrite - [in k.+1] (addn0 k) nbsurj_small //. congr (_ * _). rewrite [x in _ = x] big_ord_recl bin0. have ->: (\sum_(i < k) 'Sj(k, lift ord0 i) * 'C(n.+1, lift ord0 i) = \sum_(i < k) 'Sj(k, lift ord0 i) * 'C(n, lift ord0 i) + \sum_(i < k.+1) 'Sj(k, lift ord0 i) * 'C(n, i) ). rewrite [X in _ + X] big_ord_recr /= aux mul0n addn0 - big_split /=. by apply: eq_bigr; move => i _; rewrite binS mulnDr. rewrite addnA [X in _ = (X + _)] (_: _= \sum_(i < k.+1) 'Sj(k, i) * 'C(n, i)). by rewrite - big_split; apply eq_bigr => i _; rewrite mulnDl. by rewrite big_ord_recl bin0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)