proposition: Lemma Zeckp_prop1 (l: seq nat): uniq l -> Zeckp (Zeck_val l) = Zeck_valp l.
proof: Proof. move /sorted_gtn;set l' := (rev (sort leq l)). have hb:perm_eq (sort leq l) l by apply/permPl; apply: perm_sort. have ha: forall (l: seq nat), perm_eq (rev l) l. by elim => // a s h; rewrite rev_cons perm_rcons perm_cons. have hc: perm_eq l l' by rewrite perm_sym;apply: (perm_trans (ha _ ) hb). have ->: (Zeck_val l) = (Zeck_val l') by apply: perm_big. have ->: (Zeck_valp l) = (Zeck_valp l') by apply: perm_big. apply: Zeckp_prop0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)