proposition: Lemma FR_prop7 n (k :=Zeck_li n) (m := n - fib (k.+2)) : ~~(odd k) -> FR n = FR (Zeckpn k.+1 m) + (k./2) * FR (Zeckpn k m).
proof: Proof. rewrite /m/k; clear. case: n; first by rewrite /Zeck_li Zeck_0 /= sub0n Zeckp_0 addn0. move => n sa. set q := (Zeck_li n.+1);move: (FR_split (n:=n.+1) isT) (erefl q). rewrite -/q {6} /q -(odd_double_half q) (negbTE sa) add0n. set k := (q./2); set m := _ - _; move => [->]; case. have hu: forall k, Zeckpn k 0 = 0 by elim => // v /= ->; rewrite Zeckp_0. by move => ->; rewrite !hu FR_0 doubleK addn0 - doubleS FR_fib4 muln1 //. move => su. rewrite half_double; move: k m su; clear; elim. move => m;rewrite /= add1n addn0 => hc mz. set s := (succ_seq (Zeck m)); set n := Zeck_val s. move: (Zeck_ggen m); rewrite -sorted_ggen_succ -/s => /ZeckP ha. have ->: m = Zeckp n. by rewrite /Zeckp ha - (Zeck_zeck_val m) /Zeck_valp /Zeck_val /s !big_map. have hb: Zeck_li n = (Zeck_li m).+1. move: hc;rewrite /Zeck_li ha /s - {1} (Zeck_zeck_val m). by move: mz; case: (Zeck m) => [| u v]; rewrite ? Zeckv_nil //= last_map. have /FR_prop4 //: llen 1 (Zeck_li n) by rewrite hb /= ltnS hc. move => k Hrec m sa sb. set n := (fib (k.+1).*2.+2 + m). have mz: Zeck m != nil. apply /eqP => s. by move: (Zeck_zeck_val m) sa; rewrite /Zeck_li s Zeckv_nil => <- //. have e1: n = m + fib (k.+1).*2.+2 by rewrite addnC. have qa: ~~ odd (Zeck_li n) by rewrite /n sb odd_double. have qb: Zeck_li n != 0 by rewrite /n sb double_eq0. move: (FR_prop5 qa qb) => [qc qd]; rewrite qd in qc. rewrite doubleS in e1. move: (Zeckp_prop6 e1 (or_intror (m = 0) sa)) => [pa pb pc pd pe]. rewrite qc pe (FR_prop6 sa); rewrite mulSnr addnA; congr addn. set s2:= [seq i.-2 | i <- Zeck m]. set s1:= [seq i.-1 | i <- Zeck m]; rewrite -/s1 in pc pd. have qh : (fib k.*2.+2 + Zeckpn 2 m) = Zeckpn 2 n. have qh: fib (k.+1).*2.+1 <= fib k.*2.+3 by rewrite doubleS. by rewrite /Zeckpn /= pe pd (Zeck_split pc qh) doubleS Zeckp_fib. have qf:Zeck_li (fib k.*2.+2 + Zeckpn 2 m) = k.*2. by rewrite qh /= /Zeck_li pb // last_rcons. move:(path_all_llen pc); rewrite all_rev => qe. have qi: Zeck m = [seq i.+2 | i <- s2]. move: qe;rewrite /s1/s2; elim (Zeck m) => // a l H /= /andP [ h /H <-]. by move: h; case a => //; case. move:(path_sorted pc); rewrite rev_sorted => /ZeckP. rewrite - Zeckv_rev -pd => pf. have pg: Zeckp (Zeckp m) = Zeck_val s2. by rewrite {1} /Zeckp pf /Zeck_val /Zeck_valp /s1 qi !big_map. have ph: Zeck (Zeckp (Zeckp m)) = s2. rewrite pg; apply: ZeckP; rewrite -sorted_ggen_succ -sorted_ggen_succ. rewrite /succ_seq - map_comp /comp - qi; apply: Zeck_ggen. have qg: llen k.*2 (Zeck_li (Zeckpn 2 m)). move: qe mz; rewrite /s1 /Zeck_li ph qi /pred_seq -map_comp /comp /=. by case s2 => // a l h _ /=; move/(allP h) :(map_f succn (mem_last a l)). by rewrite -qh (Hrec _ qg qf) /Zeckpn - ! iterD // !addn2 doubleS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)