proposition: Lemma uniq_seto_to_seq B l: uniq (@seto_to_seq B l).
proof: Proof. rewrite map_inj_uniq;[ exact: enum_uniq | exact:ord_inj]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)