proposition: Lemma Zeckp_prop4b n (e := Zeckp): odd (Zeck_li n) -> (e (e n).-1).+1 = n - e n.
proof: Proof. have ->: n - e n = Zeck_valpp (Zeck n) by rewrite {1} (Zeckp_prop2 n) addKn. case: n => // n; move: (Zeck_prop1 (n:=n.+1) isT) => [a [l [ss ww ee]]]. rewrite /e /Zeck_li {2} /Zeckp /Zeck_valp /Zeck_valpp ww rev_cons last_rcons. move/oddE => ->; rewrite !sum_rcons ! sum_rev - doubleS. rewrite -fib_sum_odd_alt /Zeck_valp - big_cat /= big_cons add1n succnK. set u := ([seq i.*2 | i <- iota 1 a./2] ++ l). move: (order_path_min transitive_llen ss) => sa. have pb: all (leq 1) u. rewrite all_cat; apply /andP; split. + clear; by elim: (a./2) {2} (0) => // n H k /=. + by apply/allP => [x /(allP sa)]; case x. have pa: uniq u. rewrite cat_uniq;apply /and3P; split. + by rewrite (map_inj_uniq double_inj) iota_uniq. + apply/negP => /hasP [x /(allP sa) sb] /mapP [y]. rewrite mem_iota ltnS - (leq_double y) => /andP [_ sc] se. rewrite se in sb; move: (ltnW (leq_trans sb sc)). by rewrite ltnNge double_half_le. + apply: (uniq_llen ss). move:(fib_sum_even_alt (a./2).+1). rewrite (Zeckp_prop1_bis pb pa) /Zeck_valpp doubleS /mkseq /= big_cons add0n. by rewrite big_cat /= - addSn => ->; rewrite fib_pos. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)