proposition: Lemma Zeck_li_prop1 n : all (leq (Zeck_li n)) (Zeck n).
proof: Proof. rewrite /Zeck_li; case: n => // n. move: (Zeck_prop1 (n:=n.+1) isT) => [a [l [pa -> _]]]. rewrite rev_cons last_rcons all_rcons (leqnn) /= all_rev. by apply /allP => [x /(allP (path_all_llen pa)) /ltnW /ltnW /=]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)