proposition: Lemma Zeck_li_prop2 n k: k < (Zeck_li n) -> all [pred z | k < z] (Zeck n).
proof: Proof. by move => h; apply/allP => [x /(allP (Zeck_li_prop1 n))]; apply: leq_trans. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)