proposition: Lemma Zeckp_prop4a n (e := Zeckp): e (n + e n.-1) = n.
proof: Proof. rewrite /e; case: n => [|n]; first by rewrite !Zeckp_0. move: (Zeck_prop1 (n:=n.+1) isT) => [a [l [ss _ ->]]]. have fp: 0 < fib (a.+2) by rewrite fib_gt0. rewrite Zeckv_cons /Zeck_val; set q := \sum_(j <- l) fib j.+2. rewrite -{2}(prednK fp) addSn succnK (Zeck_split ss (leq_pred (fib a.+2))). set E1 := (fib a.+2 + Zeckp (fib a.+2).-1); set E2 := q + Zeckp q. have eq2: q = Zeckp E2 by rewrite (Zeckp_prop3a q). have eq3: E1 = if (odd a) then fib a.+3 else (fib a.+3).-1. rewrite /E1 -{1 2 4 5}(odd_double_half a); case: (odd a). rewrite add1n -doubleS Zeckp_fiba -fibSS //. rewrite - doubleS Zeckp_fibc doubleS succnK. by rewrite (fibSS (a./2).*2.+1) {2} (fib_pos (a./2).*2) addnS. have eq4: fib a.+2 = Zeckp E1. rewrite eq3; case h: (odd a); first by rewrite (oddE h) Zeckp_fib. by rewrite (evenE h) - doubleS Zeckp_fiba. move:(Zeckp_prop2_bis l) => [ha hb]. have <-: Zeckp q = Zeck_valp l by apply: Zeckp_prop1;apply: (uniq_llen ss). rewrite addnACA /E2 /q; move => ->; rewrite -/(Zeck_val l) - ha; symmetry. rewrite (Zeck_split (a := a.+1)) => //. + by rewrite - eq4 // Zeckp_prop1 // (map_inj_uniq succn_inj) (uniq_llen ss). + by move: ss; rewrite - map_cons -sorted_llen_succ. + by rewrite -/E1 eq3; case: (odd a) => //; apply: leq_pred. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)