proposition: Lemma FR_fib6 k: FR (fib (k.+2).*2.+1).-2 = (FR (fib (k.+2).*2).-2).+1.
proof: Proof. move: (Zeck_fib4 k.+1); rewrite /mkseq /= iota_S - map_comp /comp. set s := [seq (x.+1).*2.+2 | x <- iota 0 k] => eq1. set m := Zeck_val s. rewrite FR_prop8; set n := (fib (k.+2).*2.+1).-2. rewrite /Zeck_li eq1 rev_cons last_rcons /= mul1n. have ->: (n - fib 0.*2.+4) = m. by rewrite - (Zeck_zeck_val n) /n eq1 Zeckv_rev Zeckv_cons addKn. set s1 := [seq (x.+1).*2.+1 | x <- iota 0 k]. set s2 := [seq (x.+1).*2 | x <- iota 0 k]. have eq2 : s = [seq i.+1 | i <- s1] by rewrite /s /s1 - map_comp. have eq3 : s1 = [seq i.+1 | i <- s2] by rewrite /s1 /s2 - map_comp. have ha: sorted llen s2 by apply:sorted_llen_mkseq => u /=; rewrite !ltnS. have hb: sorted llen s1 by rewrite eq3 sorted_llen_succ. have hc: sorted llen s by rewrite eq2 sorted_llen_succ. have eq4: Zeck m = rev s. by rewrite /m - Zeckv_rev; apply: ZeckP; rewrite rev_sorted. have eq5: Zeckp m = Zeck_val s1. by rewrite /Zeckp eq4 /Zeck_val /Zeck_valp sum_rev eq2 big_map. have eq6: Zeck (Zeckp m) = rev s1. by rewrite eq5 - Zeckv_rev; apply: ZeckP; rewrite rev_sorted. have eq7: Zeckp (Zeckp m) = Zeck_val s2. by rewrite /Zeckp eq6 /Zeck_val /Zeck_valp sum_rev eq3 big_map. have eq8: Zeck (Zeckp (Zeckp m)) = rev s2. by rewrite eq7 - Zeckv_rev; apply: ZeckP; rewrite rev_sorted. have eq9: (Zeck_valp (rev s2)) = (fib (k.+1).*2).-1. rewrite Zeckvp_rev - fib_sum_odd_alt /mkseq /= /s2 Zeckvp_cons /=. rewrite iota_S - map_comp //. have eq10 :(Zeck_val s2) = (fib k.*2.+3).-2. by rewrite - Zeckv_rev - (Zeck_fib4 k) Zeck_zeck_val. by rewrite {1} /Zeckp eq8 eq7 eq9 FR_fib3 eq10 -FR_fib5. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)