proposition: Lemma Zeck_S k n: fib k.+2 <= n < fib k.+3 -> Zeck n = k :: Zeck (n - fib k.+2).
proof: Proof. case: n => [|n bd]; first by rewrite leqn0 fib_eq0. move /eqP: (fib_partition (fib_contentP n) bd); rewrite eqSS eqSS Zeck_S'. by move/eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)