proposition: Lemma seq_to_setoK B (l: seq nat): uniq l -> (all (fun z => z < B.+1) l) -> perm_eq (seto_to_seq (seq_to_seto B l)) l.
proof: Proof. move => ul /allP bl. rewrite /seq_to_seto/seto_to_seq. apply: uniq_perm => //. rewrite map_inj_uniq; [ apply: enum_uniq | apply: ord_inj]. move => x; apply/mapP/idP. move=> [i]; rewrite mem_enum => /imsetP [j /mapP [k kl ->] ->] ->. by rewrite inordK //; apply: bl. move => xl; exists (inord x); last by rewrite inordK //; apply: bl. by rewrite mem_enum; apply /imsetP; exists (inord x) => //; apply: map_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)