proposition: Lemma Zeckp_prop0 l: sorted gtn l -> Zeckp (Zeck_val l) = Zeck_valp l.
proof: Proof. by move /Zeckp_prop00 => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)