proposition: Lemma Zeckp_le n: Zeckp n <= n ?= iff (n <= 1).
proof: Proof. apply/leqifP; case:n => [ | [ | n]]; rewrite ? Zeckp_0 ? Zeckp_1 //=. rewrite {2} (Zeckp_prop2 n.+2); apply: ltn_paddr. rewrite Zeck_S' /Zeck_valpp big_cons; move: (fib_contentP n.+1) => /=. case: (fib_content n.+1); [ rewrite !ltnS // | move => k _]. by rewrite addn_gt0 fib_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)