proposition: Lemma ZeckM_prop4 n l: sorted gtn l -> Zeck_val l = n -> (size (Zeck n) <= size l <= size (ZeckM n) /\ (size (Zeck n) = size (ZeckM n) -> l = (Zeck n))).
proof: Proof. move => pa pb. move: (ZeckM_is_maximal pa pb) => [pc pd]. move: (Zeck_is_minimal pa pb) => [pe pf]. by rewrite pc pe; split => // h;apply /eqP; rewrite - pf eqn_leq pe h pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)