proposition: Lemma ZeckM_is_maximal n l: sorted gtn l -> Zeck_val l = n -> size l <= size (ZeckM n) ?= iff (l == (ZeckM n)).
proof: Proof. move: (ZeckM_prop1 n) => [ha hb whc]. rewrite (Zeck_zeck_val n) in hb. move => /max_rep_prop1 [s [hc hd /leqifP M]] he. case wx: (spec_sorted l). by rewrite hb in he; rewrite (max_rep_unique wx ha he); apply/leqif_refl. apply/leqifP; move: M; rewrite he hb in hd;rewrite wx (max_rep_unique ha hc hd). by case H: (l==s) => //; rewrite (eqP H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)