proposition: Lemma foo2 n: br n.+1 n = 'St(n.+2,n.+1).
proof: Proof. rewrite /br 2!big_ord_recr /= binn mul1n big1; last first. by move => i _; rewrite stir_small1 ?muln0. by rewrite add0n stirS binSn 2!stir_nn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)