proposition: Lemma Zeckp_prop1_bis l: all (leq 1) l -> uniq l -> Zeckp (Zeck_valp l) = Zeck_valpp l.
proof: Proof. move => sb; rewrite (seq_prednK sb) /Zeck_valp /Zeck_valpp /succ_seq. move/ map_uniq; rewrite big_map big_map; apply:Zeckp_prop1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)