fact: Fixpoint FA_rec (m n k:nat) := if k is k'.+1 then if (m==0) then (n==0): nat else if n < m then 0 else FA_rec (n-m) m k' + FA_rec (n - m) (m-1) k' else 0.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)