proposition: Lemma FR_unique n: FR n = 1 -> exists k, n = (fib k.+2).-1.
proof: Proof. have H k: FR k = 1 -> ((Zeck_li k)./2) = 0. rewrite {1} FR_prop8. case: (posnP (Zeck_li k)./2) => // ha. set u := Zeckpn _ _; set v := Zeckpn _ _ => eq1. have hb: 0 < (Zeck_li k)./2 * FR v by rewrite muln_gt0 ha (FR_positive v). by move: (leq_add (FR_positive u) hb); rewrite eq1. have H0: exists k, 0 = (fib k.+2).-1 by exists 0. elim: n {-2} (n) (leqnn n); first by move => n; rewrite leqn0 => /eqP ->. move => b Hr n nb fz1. case (posnP n); [by move => -> | move => np]. have H1: forall m, Zeckp m <= m. move => m; rewrite /Zeckp -{2} (Zeck_zeck_val m) /Zeck_val /Zeck_valp. elim: (Zeck m); first by rewrite !big_nil. move => a l HH; rewrite !big_cons leq_add // ? fib_monotone //. have H2: forall n m, Zeckpn n m <= m. elim => // n1 HH m; exact (leq_trans (H1 (Zeckpn n1 m)) (HH m)). have n1b: n.-1 <= b by rewrite - ltnS (prednK np). move: (H _ fz1) => fz2. move: fz1; rewrite FR_prop8 fz2 addn0; set k := Zeck_li n. have nnz: n != 0 by rewrite -lt0n. move:(Zeck_prop1 nnz) => [a[l [pa pb pc]]]. have ak: a = k by rewrite /k /Zeck_li pb rev_cons last_rcons. have: n - fib k.+2 = Zeck_val l by rewrite pc Zeckv_cons ak addKn. have ul := (uniq_llen pa). have lge2: all (leq a.+2) l by apply /allP => [x /(allP(path_all_llen pa))]. have: all (leq 1) l by apply /allP => [x /(allP lge2) ]; case: x. move/ (seq_prednK); set s := (pred_seq l) => sv. have ss: sorted llen s by rewrite - sorted_llen_succ - sv (path_sorted pa). have: (k == 0) || (k == 1) by move: fz2; rewrite -/k; case k => // [] []. case /orP => /eqP kz; rewrite kz. have aa: (Zeckpn 1 (n - fib 2)) <= b. by apply:(leq_trans (H2 1 (n - fib 2))); rewrite subn1. move => eqa /(Hr _ aa) [u]; rewrite /Zeckpn /= eqa => eqb. have: rev (Zeck (Zeckp (Zeck_val l))) = s. rewrite -(revK s) (Zeckp_prop1 ul) sv /Zeck_valp big_map - sum_rev ZeckP //. by rewrite rev_sorted. rewrite eqb -(odd_double_half u); case: (odd u). rewrite add1n - doubleS Zeck_fib1 revK => h. have /(allP lge2) //: 1 \in l by rewrite sv (mem_map succn_inj) - h. rewrite Zeck_fib2 revK => sv2; exists ((u./2)).*2.+1. rewrite pc ak kz sv -sv2 /succ_seq -map_comp /comp -doubleS. by rewrite -fib_sum_even_alt2 /mkseq /= iota_S - !map_comp. have aa: Zeckpn 2 (n - fib 3) <= b. apply:(leq_trans (H2 2 (n - fib 3))); rewrite subn2. exact(leq_trans (leq_pred n.-1) n1b). move => eqa /(Hr _ aa) [u]; rewrite /Zeckpn /= eqa => eqb. have: all (leq 1) s. by apply/allP => [x/mapP [y /(allP lge2) y2] ->];move: y2; case y => // [] []. move/ (seq_prednK); set s' := pred_seq s => sv'. have eq1 :=(Zeckp_prop1 (uniq_llen pa)). have eq2: (Zeck (Zeckp (Zeck_val l))) = rev s. rewrite eq1 sv /Zeck_valp big_map - sum_rev ZeckP //. by rewrite rev_sorted - sorted_llen_succ - sv (path_sorted pa). have : rev (Zeck (Zeckp (Zeckp (Zeck_val l)))) = s'. rewrite -(revK s') {1}/Zeckp eq2 sv' /Zeck_valp sum_rev big_map. by rewrite - sum_rev ZeckP // rev_sorted - sorted_llen_succ - sv'. rewrite eqb -(odd_double_half u); case: (odd u). rewrite add1n - doubleS Zeck_fib1 revK => sv2. have: 2 \in l by rewrite sv sv' /succ_seq -map_comp;apply/map_f; rewrite -sv2. by move/(allP lge2); rewrite ak kz. rewrite Zeck_fib2 revK => sv2; exists ((u./2).+1).*2. rewrite pc - doubleS -fib_sum_odd_alt sv sv' - sv2 ak kz. by rewrite /Zeck_val/Zeck_valp /mkseq/= !iota_S ! big_cons ! big_map succnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)