proposition: Lemma Zeckv_pos n l: 0 < Zeck_val (n ::l).
proof: Proof. by rewrite Zeckv_cons 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)