proposition: Lemma ZeckM_prop3 n l: max_rep n l -> ZeckM n = l.
proof: Proof. move:(ZeckM_prop2 n) => /andP[ha /eqP hb] /andP[hc /eqP hd]. by apply:max_rep_unique => //; rewrite hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)