fact: Fixpoint stirling2_rec n m := match n, m with | n'.+1, m'.+1 => m *stirling2_rec n' m + stirling2_rec n' m' | 0, 0 => 1 | 0, _.+1 => 0 | _ .+1, 0 => 0 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)