fact: Fixpoint Zeck_rec n k:= if k is k'.+1 then if n is n'.+1 then let r := fib_content n' in r:: Zeck_rec (n - (fib (r.+2))) k' else nil else nil.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)