proposition: Lemma FR_rec n (e := Zeckp n): n != 0 -> FR n = FA(n -e) e + FA (n-e) e.-1.
proof: Proof. rewrite /FR/e -Zeckp_eq0 - lt0n => /prednK => eq. move: (Zeckp_le n) => [/subnKC sa sb]. by move: (FA_gen (Zeckp n).-1 (n - Zeckp n)); rewrite eq sa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)