proposition: Lemma Zeckp_prop2_bis l (s := [seq i.+1 | i <- l]): [/\ Zeck_valp s = Zeck_val l, Zeck_valpp s = Zeck_valp l & Zeck_val l + Zeck_valp l = Zeck_val s].
proof: Proof. by rewrite (Zeck_valppE s) /s /Zeck_valp /Zeck_val /Zeck_valpp !big_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)