proposition: Lemma stir_SSnn n: 'St(n.+2, n) = 'C(n.+3,4) + 2 * 'C(n.+2,4).
proof: Proof. elim:n => [// | n Hrec]; rewrite stirS Hrec stir_Snn addnCA (binS (n.+3)). rewrite -addnA; congr (_ + _). rewrite (binS (n.+2) 3) (addnC 'C(n.+2, 4)) mulnDr addnA; congr (_ + _). by rewrite (binS (n.+2) 2) addnC addnA mulSnr -addn2 mul_Sm_binm_1 mulSnr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)