proposition: Lemma Zeck_li_pr n: n != 0 -> Zeck_li n < n.
proof: Proof. move: (Zeck_val_bounded1 n); rewrite/Zeck_li;case: n => // n. by rewrite (Zeck_S' n) => sa sb; apply: (allP sa); simpl; apply:mem_last. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)