proposition: Lemma ZeckM_prop1 n: [/\ spec_sorted (ZeckM n), Zeck_val (Zeck n) = Zeck_val (ZeckM n) & size (Zeck n) <= size (ZeckM n) ?= iff spec_sorted (Zeck n)].
proof: Proof. exact :(svalP (max_rep_prop1 (sorted_ggenW (Zeck_ggen n)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)