fact: Fixpoint ffact_rec n m := if m is m'.+1 then n * ffact_rec n.-1 m' else 1.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)