proposition: Lemma FR_prop5 n: ~~ odd (Zeck_li n) -> (Zeck_li n) != 0 -> FR n = FR (Zeckp n) + FR((Zeckp n).-1) /\ FR (Zeckp n) = FR (Zeckpn 2 n).
proof: Proof. pose qk n := fib (Zeck_li n).+2;pose pk n := (n - qk n). move => ha hb. have nz: n != 0 by apply /negP => /eqP nz; move: hb; rewrite nz /Zeck_li Zeck_0. move: (FR_split nz); set m := _ - _; set p := fib _; move => [pb pc]. set k := (Zeck_li n)./2.-1. have pq: (Zeck_li n) = (k.+1).*2. move: hb; rewrite - (odd_double_half (Zeck_li n))(negbTE ha) add0n. by rewrite double_eq0 -lt0n => /prednK => <-. move: pb; rewrite addnC /p pq doubleS => pb; rewrite pq in pc. rewrite (FR_prop0 hb); case: pc => pc. by rewrite pb pc add0n {3} /FR /= !Zeckp_fib FR_fib1 -! doubleS Zeckp_fiba. move: (Zeckp_prop6 pb (or_intror (m = 0) pc)) => [qa _ qc qd qe]. split. rewrite /FR;congr addn; congr FA. have: 0 < fib k.*2.+3 by rewrite fib_gt0. have qx := leqnn (fib (k.+1).*2.+1); have qy:= leq_pred (fib (k.+1).*2.+1). move/prednK => xx; rewrite qe -{2} xx addSn succnK qd. by rewrite (Zeck_split qc qx) (Zeck_split qc qy) Zeckp_fiba doubleS Zeckp_fib. by apply: FR_prop3; rewrite /Zeck_li qa last_rcons /= odd_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)