proposition: Lemma FR_fib3 k: FR (fib k).-1 = 1.
proof: Proof. have h0:= FR_0; have h1:= FR_1. suff H: forall k, FR (fib k.*2).-1 = 1 /\ FR (fib k.*2.+1).-1 = 1. move: (H k./2) => [sa sb]; rewrite - (odd_double_half k); case (odd k) => //. clear k; case => //;elim => // n []; set k := n.+1 => sa sb. set l := succ_seq [seq i.*2 | i <- iota 0 k]. have eq1: [seq i.*2 | i <- iota 1 k] = [seq i.+1 |i <- l]. by rewrite /l iota_S - !map_comp /comp. have ea: Zeck (Zeck_val l) = rev l. rewrite -{1} (revK l) /Zeck_val sum_rev; apply: ZeckP. by rewrite rev_sorted /l sorted_llen_succ sorted_llen_mkseq_e. have eb : Zeck_val l = (fib (k.+1).*2).-1. by rewrite - fib_sum_odd_alt /Zeck_valp /mkseq map_cons big_cons eq1 big_map. have res1:FR (Zeck_val l) = 1. have ha:odd (Zeck_li (Zeck_val l)). by rewrite /Zeck_li ea /l /succ_seq -map_comp /k /= rev_cons last_rcons. by rewrite (FR_prop3 ha) eb Zeckp_fibc doubleS. split; first by rewrite - eb. set u:= [seq i.+2 | i <- l]. have ec: Zeck (Zeck_val u) = rev u. rewrite -{1} (revK u) /Zeck_val sum_rev /u/l - map_comp /comp - map_rev. apply: ZeckP. rewrite map_rev rev_sorted - map_comp sorted_llen_mkseq //. by move => x; rewrite doubleS /=. have ed: llen 1 (Zeck_li (Zeck_val u)). by rewrite /Zeck_li ec /u /l - !map_comp /comp /k /= rev_cons last_rcons. have ee: Zeckp (Zeck_val u) = Zeck_val (rev ([seq i.+1 | i <- l])). by rewrite /Zeckp ec /Zeck_valp /Zeck_val ! sum_rev /u ! big_map. rewrite - fib_sum_even_alt2 /mkseq map_cons eq1 /Zeck_val big_cons add1n. move: (FR_prop4 ed); rewrite ee /Zeck_val sum_rev - res1 => ->; congr FR. have uu:uniq u. rewrite /u /l - !map_comp /comp map_inj_uniq ?iota_uniq//. by move => x y /= /eqP; rewrite !eqSS eqn_double => /eqP. have au: all (leq 1) u by apply/allP => x /mapP [y yl ->]. move: (Zeckp_prop1_bis au uu). by rewrite /u /Zeck_val /Zeck_valp /Zeck_valpp !big_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)