proposition: Lemma ZeckMgt2 n: 2 <n -> 2 <= size (ZeckM n).
proof: Proof. move/andP:(ZeckM_prop2 n)=> []; case: (ZeckM n). by rewrite Zeckv_nil => _ /eqP <-. move => a l; rewrite spec_sorted_rec /= ltnS; case:l => //=. by rewrite Zeckv_cons Zeckv_nil leqn1 => /andP []; case/orP=> /eqP -> _ /eqP <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)