proposition: Lemma Zeck_odd_last_prop l: sorted gtn l -> odd_last(Zeck (Zeck_val l)) = odd_last 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)