proposition: Lemma Zeck_S' n (r := fib_content n) : Zeck n.+1 = r :: (Zeck (n.+1 - (fib (r.+2)))).
proof: Proof. have Ha := fib_content_large. suff aux: forall m n k1 k2, m <= k1 -> m <= k2 -> n <= m -> Zeck_rec n k1 = Zeck_rec n k2. by congr cons; apply: (aux (n.+1 - fib (fib_content n).+2)). clear n r. elim; first by move => n k1 k2 _ _;rewrite leqn0 => /eqP ->; case: k1; case: k2. move => m Hrec n; case => // k1; case => // k2; rewrite (leq_eqVlt n) ! ltnS. move => mk1 mk2 /orP [ /eqP ->| lenm]; first by congr cons; apply:Hrec. by apply: Hrec => //; apply: ltnW; rewrite ltnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)