proposition: Lemma FR_prop1 n: Zeck_li n.+1 = 0 -> FR n.+1 = FR (Zeckp n).
proof: Proof. case: n; first by rewrite Zeckp_0 FR_1 FR_0. move => n; rewrite FR_rec // => /Zeckp_prop5 /= /and3P [ea /eqP ec /eqP eb]. move:(Zeckp_prop3b ea) => ed. by rewrite {1 3 4} eb subSS -(Zeckp_prop3b ea) -/(FR _) (FA_prop0 ec). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)