proposition: Lemma FR_prop3 n: odd (Zeck_li n) -> FR n = FR (Zeckp n).
proof: Proof. move => h. have H1: Zeck_li n != 0. by move: h; rewrite/ Zeck_li;case : (last n (Zeck n)). by rewrite (FR_prop0 H1) (Zeckp_prop3b H1) - (Zeckp_prop4b h) FA_prop0bis ?addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)