proposition: Lemma stir1_S n m : 'So(n.+1, m.+1) = n * 'So(n, m.+1) + 'So(n, m).
proof: Proof. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)