proposition: Lemma Zeckp_prop5 n (e := Zeckp): Zeck_li n.+1 = 0 -> (n == 0) || [&& (Zeck_li n != 0), e (e n.+1) == (e (e n)).+1 & (e (n.+1) == (e n).+1)].
proof: Proof. move: (Zeck_prop1 (n:=n.+1) isT) => [a [l [pa]]]. move: (path_all_llen pa) => ha. have ha': all (leq 1) l by apply/allP => [x /(allP ha)]; case x. rewrite /Zeck_li /e /Zeckp /Zeck_valp rev_cons => pb; rewrite pb. rewrite last_rcons /Zeck_val => sa sb. move: sa; rewrite sb !sum_rcons big_cons !add1n => /eqP. rewrite !eqSS => /eqP sa. have sr: sorted ggen (rev l) by rewrite rev_sorted; exact (path_sorted pa). have eq1 : Zeck n = rev l by rewrite sa -sum_rev; apply:ZeckP. rewrite {1} sa eq1 eqxx sum_rev. case rvz: (l == nil); first by rewrite (eqP rvz) big_nil. have ->: last n (rev l) != 0. by move: ha rvz; case l => // b s; rewrite rev_cons last_rcons /=; case b. rewrite andbT /=;apply/orP; right. move: (seq_prednK ha'). set m := (\sum_(i <- l) fib i.+1); set w := (pred_seq l) => hb. have sa1: sorted ggen (rev w). move: sr; rewrite hb !rev_sorted sorted_llen_succ //. have nv: m = Zeck_val (rev w) by rewrite /m /Zeck_val hb big_map sum_rev. have ->: Zeck m = (rev w) by rewrite nv; apply:ZeckP. have ->: m.+1 = Zeck_val (rcons (rev w) 0) by rewrite /Zeck_val sum_rcons nv. rewrite [X in X == _] (Zeckp_prop1) ? /Zeck_valp ? sum_rcons //. rewrite rcons_uniq (sorted_ggen_uniq sa1) andbT; apply/negP. rewrite mem_rev => /mapP [x /(allP ha)]; case x => // [] [] //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)