fact: Fixpoint fib_rec n := if n is n1.+1 then if n1 is n2.+1 then fib_rec n1 + fib_rec n2 else 1 else 0.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)