proposition: Lemma Zeckp_prop00 l: sorted gtn l -> Zeckp (Zeck_val l) = Zeck_valp l /\ odd_last(Zeck (Zeck_val l)) = odd_last l.
proof: Proof. move => h;rewrite /Zeckp; apply: Zeck_valp_same => //. apply: sorted_ggenW; apply:Zeck_ggen. exact:Zeck_zeck_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)