proposition: Lemma Zeck_val_bounded1 n: all (fun i => i < n) (Zeck n).
proof: Proof. apply/allP => x /(allP (Zeck_val_bounded n)) h. exact: (leq_trans (fib_gen x.+1) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)