proposition: Lemma FR_positive n: 0 < FR n.
proof: Proof. elim: n {-2} n (leqnn n). by move => n; rewrite leqn0 => /eqP ->; rewrite FR_0. move => n IH n1; rewrite leq_eqVlt; case/orP=> [|Hn]; last first. by apply: IH; rewrite -ltnS. move => /eqP => ->; case h:(Zeck_li n.+1 == 0). by move: (Zeckp_le n) => [/ IH ha hb]; rewrite (FR_prop1 (eqP h)). move:(FR_prop0 (negbT h)) IH; clear h; case: n; first by rewrite FR_1. move => n -> h; move /leqifP: (Zeckp_le n.+2) => /=; rewrite ltnS => /h lt. by apply: (leq_trans lt); rewrite leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)