proposition: Lemma foo3 n: br n.+2 n = 'St(n.+3,n.+1).
proof: Proof. rewrite /br 3!big_ord_recr /= binn mul1n big1; last first. by move => i ; rewrite stir_small1 ?muln0. rewrite add0n stirS binS binn mulnDl mul1n -addnA binSn stir_nn muln1. rewrite addnA addnA stir_Snn (_: 'C(n.+2, n) + 'C(n.+1, 2) = n.+1 *n.+1). rewrite - mulnDr stirS stir_nn muln1 stir_Snn //. by rewrite -addn2 binom_mn_n addn2 binS addnAC addnn - muln2 bin2' bin1 mulSnr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)