proposition: Lemma FR_prop6 k m: llen (k.+1).*2 (Zeck_li m) -> FR (fib (k.+1).*2.+1 + Zeckp m).-1 = FR (Zeckpn (k.+1).*2 m).
proof: Proof. rewrite (fib_pos) addSn succnK. elim: k m => [m mv | k Hrec m mv]; first by apply:(FR_prop4 (ltnW mv)). have ->: (Zeckpn (k.+2).*2 m) = ((Zeckpn (k.+1).*2 (Zeckp (Zeckp m)))). by elim k => // k1 /= ->. set RHS := RHS. move:(Zeckp_prop6 (erefl ( m + fib (k.+1).*2.+4)) (or_intror (m = 0) mv)). move => [_ _ pc pd _]. rewrite - fib_sum_even_alt2 /mkseq /= /Zeck_val big_cons addSn. set l := pred_seq (Zeck m) ++ rev ([seq i.*2 | i <- iota 1 k.+1]). set x := _ + _; have {x} -> : x = Zeck_val l. by rewrite /x/l pd /Zeck_val big_cat !sum_rev /= addnC. set lp := succ_seq l. have ha: sorted ggen (rcons l 0). have pa3 n a b: (last a [seq i.*2 | i <- iota b n.+1]) = (n + b).*2. by elim: n a b => // n H a b;move: (H 0 b.+1); rewrite addnS addSn. have pa2: sorted llen ((k.+1).*2 :: rev [seq i.-1 | i <- Zeck m]). by move:pc; case: (rev _) => // a s /=/andP[/ltnW /= -> ->]. rewrite /l - rev_sorted rev_rcons rev_cat revK /= cat_path. move:(sorted_llen_mkseq_e 1 k.+1) => /= ->. by move: pa2;case k => // k'; rewrite pa3 addn2. have hb: sorted ggen l. move: ha;rewrite - rev_sorted -(rev_sorted _ l) rev_rcons /=. by move /path_sorted. move:(sorted_ge2_all_ps ha) => [hc hd]. move: (seq_prednK hd); set l' := (pred_seq l) => sv. have hd' : all (leq 1) l'. move: hc; rewrite /l' => h; apply/allP => [x /mapP [y /(allP h) u ->]]. by move: u; case y => //. move: (seq_prednK hd'); set l'' := pred_seq l' => sv'. have he: sorted ggen l' by rewrite - sorted_ggen_succ - sv. have he': sorted ggen l'' by rewrite - sorted_ggen_succ - sv'. have ea: Zeck_val l = Zeck_valp lp by rewrite /Zeck_val /Zeck_valp big_map. have eb: Zeck (Zeck_val lp) = lp by apply: ZeckP; rewrite sorted_ggen_succ. have ec: Zeck (Zeck_val l) = l by apply: ZeckP. have ed: Zeckp (Zeck_val lp) = Zeck_val l by rewrite /Zeckp eb - ea. have ee: Zeck (Zeck_val l') = l' by apply: ZeckP. have ef: (Zeck_valp l) = Zeck_val l'. by rewrite /Zeck_val /Zeck_valp sv big_map. have eg: Zeck (Zeck_valp l) = l' by rewrite ef; apply:ZeckP. have hf: llen 1 (Zeck_li (Zeck_val lp)). rewrite /Zeck_li eb /lp /l /succ_seq map_cat map_rev - ! map_comp /=. by rewrite last_cat rev_cons last_rcons. have eh: Zeck_li (Zeck_valp l) = 1. rewrite /Zeck_li eg /l' /l /pred_seq map_cat map_rev - !map_comp /comp /=. by rewrite last_cat ! rev_cons last_rcons. move: pc pd; set s := rev (pred_seq (Zeck m)) => pc pd. have us:= (uniq_llen pc). have ei: Zeckp (Zeckp m) = Zeck_valp s by rewrite pd; apply: Zeckp_prop1. have sb1: all (leq (k.+1).*2.+3) s. move: pc; elim:(s) => // a L H /=/andP [h1 h2]; rewrite h1 /=; apply:H. by move:h2; case:L => // a' L' /= /andP [/ltnW /(ltn_trans h1) -> ->]. have sb2: all (leq 1) s by apply/allP => [ x /(allP sb1)]; case:x. have sb3: all (leq 2) s by apply/allP => [ x /(allP sb1)]; case:x => //; case. move: (seq_prednK sb2); set s' := (pred_seq s) => s'v. have ek: Zeck (Zeck_valp s) = rev s'. rewrite /Zeck_valp s'v big_map - sum_rev; apply:ZeckP. rewrite rev_sorted - sorted_llen_succ - s'v; exact:(path_sorted pc). have ej: Zeckp (Zeckp (Zeckp m)) = Zeck_valpp s. by rewrite ei Zeckp_prop1_bis. have hi:llen (k.+1).*2 (Zeck_li (Zeckp (Zeckp m))). move: mv sb1;rewrite /Zeck_li ei ek /s' /s -{1} (Zeck_zeck_val m). case: (Zeck m); first by rewrite /= Zeckv_nil //. move => a l1 _; rewrite /pred_seq map_rev revK - map_comp /comp all_rev => w. set y := last a.-2 [seq x.-2 | x <- l1];rewrite /= -/y. have: y\in [seq x.-2 | x <- a::l1] by rewrite /y map_cons; apply:mem_last. move /mapP => [x /(map_f predn) /(allP w) xh ->]. by move: xh; case x => //; case => //. have aa:(Zeck_valp l') = Zeck_valpp l. by rewrite /Zeck_valp /Zeck_valpp sv /succ_seq big_map. have: odd (Zeck_li (Zeck_valp l)) by rewrite eh. rewrite - ed (FR_prop4 hf) ed /Zeckp ec; move /FR_prop3 => ->. rewrite /Zeckp eg aa /Zeck_valpp /l big_cat /= - sum_rev -/s addnC sum_rev. rewrite - map_cons -/(iota 1 k.+1) /RHS - (Hrec _ hi) ej; congr (FR (_ + _)). by rewrite -(fib_sum_even_alt k.+2) /Zeck_valpp /mkseq /= !big_cons /= add0n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)