proposition: Lemma seto_to_seqK B (s: {set 'I_B.+1}) : seq_to_seto B (seto_to_seq s) = s.
proof: Proof. rewrite /seq_to_seto/seto_to_seq - map_comp /comp. apply/setP =>i; apply/imsetP/idP. by move => [x /mapP [y ]]; rewrite mem_enum inord_val => ys -> ->. move => h; rewrite - (inord_val i);exists (inord i) => //. by apply: map_f; rewrite mem_enum. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)