proposition: Theorem FR_prop8 n (k :=Zeck_li n) (m := n - fib (k.+2)) : FR n = FR (Zeckpn k.+1 m) + (k./2) * FR (Zeckpn k m).
proof: Proof. case ok: (odd k); last by rewrite (FR_prop7 (negbT ok)). move: (prednK (odd_gt0 ok)) => eq1. have opk: ~~(odd k.-1) by move: ok;rewrite - eq1. case nz: (n ==0); first by move: eq1; rewrite /k (eqP nz) /Zeck_li. move: (Zeck_prop1 (negbT nz)) => [a [l [pa pb pc]]]. have eq2: a = k by rewrite /k /Zeck_li pb rev_cons last_rcons. rewrite eq2 in pa pb pc. have eq3: m = Zeck_val l by rewrite /m pc Zeckv_cons addKn. have: all (leq 1) l by apply/allP => [x /(allP (path_all_llen pa))]; case x. move/seq_prednK; set s := pred_seq l => sv. have pd:= (path_sorted pa). have eq4: Zeck m = rev l. by rewrite eq3 - Zeckv_rev; apply: ZeckP; rewrite rev_sorted. have pe: (Zeck_val l) = 0 \/ llen k.-1.+1 (Zeck_li (Zeck_val l)). move: ok pa;rewrite /Zeck_li - eq3 eq4 {1} eq3; case l => [_ _ | x y]. by left; rewrite Zeckv_nil. by rewrite rev_cons last_rcons /=; case k => // k' _ /andP [ h];right. move: (pc); rewrite Zeckv_cons addnC - eq1 => pc'. move: (Zeckp_prop6 pc' pe); rewrite - eq3; move => [pf _ pg ph pi]. have eq5: (Zeck_li (fib k.-1.+2 + Zeckp m)) = k.-1. by rewrite /Zeck_li -pi pf last_rcons. have opk1: ~~odd (Zeck_li(fib k.-1.+2 + Zeckp m)) by rewrite eq5. rewrite (FR_prop3 ok) pi (FR_prop7 opk1) eq5 addKn. by rewrite /Zeckpn !iterSr (evenE (negbTE opk)) doubleK /= uphalf_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)