proposition: Lemma FR_prop0 n: Zeck_li n != 0 -> FR n = FR (Zeckp n) + FA (Zeckp (Zeckp n)) (Zeckp n).-1.
proof: Proof. case h: (n==0); first by rewrite (eqP h) /Zeck_li Zeck_0. by move =>h1;rewrite (FR_rec (negbT h)) -(Zeckp_prop3b h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)