proposition: Lemma FR_fib5 k: FR (fib k.*2.+4).-2 = FR(fib k.*2.+3).-2.
proof: Proof. rewrite - !doubleS; move: (Zeck_fib3 k). set n := (fib (k.+2).*2).-2 => zn. set m := Zeck_val (mkseq (fun i : nat => i.*2.+3) k). have eq2: n = m.+1 by rewrite - (Zeck_zeck_val n) zn Zeckv_rev Zeckv_cons. have eq1: (Zeck_li m.+1 = 0) by rewrite /Zeck_li - eq2 zn rev_cons last_rcons. have ul: uniq (mkseq (fun i => i.*2.+3) k). by apply: mkseq_uniq => u v /eqP; rewrite !eqSS eqn_double => /eqP. rewrite eq2 (FR_prop1 eq1) /m (Zeckp_prop1 ul). rewrite - (Zeck_zeck_val ((fib (k.+1).*2.+1).-2)) (Zeck_fib4 k) Zeckv_rev. by rewrite /Zeck_val/Zeck_valp /mkseq !big_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)