proposition: Lemma nbsurjS n m : 'Sj(n.+1, m.+1) = (m.+1) * ('Sj(n, m.+1) + 'Sj(n, m)).
proof: Proof. by rewrite /nbsurj stirS mulnDr mulnDl - ! mulnA (mulnCA _ _ m`!) factS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)