proposition: Lemma FR_fib4 k: FR (fib k.*2) = k.-1.+1.
proof: Proof. elim: k => [| k H]; first by rewrite FR_0. have h: Zeck_li (fib (k.+1).*2) = k.*2 by rewrite /Zeck_li doubleS Zeck_fib /=. have ei: ~~ odd (Zeck_li (fib (k.+1).*2)) by rewrite h odd_double. case kz: (k == 0); [by rewrite (eqP kz) FR_1 | move: (negbT kz) => kp]. have mz: Zeck_li (fib (k.+1).*2) != 0 by rewrite h double_eq0 kp. rewrite (proj1 (FR_prop5 ei mz)) doubleS Zeckp_fib FR_fib2 H FR_fib3 addn1. by rewrite /= prednK // lt0n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)