proposition: Lemma stir1_Snn n: 'So(n.+1, n) = 'C(n.+1,2).
proof: Proof. elim:n => [//|n IHn]. by rewrite stir1_S IHn stir1_nn muln1 addnC (binS (n.+1)) bin1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)