proposition: Lemma Zeck_valp_same (l1 l2: seq nat): sorted gtn l1 -> sorted gtn l2 -> Zeck_val l1 = Zeck_val l2 -> Zeck_valp l1 = Zeck_valp l2 /\ odd_last l1 = odd_last l2.
proof: Proof. move /Zeck_valp_aux => [l3 [pa -> -> -> _]] /Zeck_valp_aux [l4 [pb -> -> -> _]]. by move/(Zeck2_unique pa pb) ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)