proposition: Lemma Zeck_val_bounded n: all (fun i => fib i.+2 <= n) (Zeck n).
proof: Proof. rewrite - {1} (Zeck_zeck_val n) /Zeck_val; elim: (Zeck n) => // a l H. rewrite /= big_cons leq_addr /=;apply /allP => [x /(allP H) h]. by apply: (leq_trans h); rewrite leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)