proposition: Lemma enum_val_full : x \subset p -> x = [set @enum_val _ (mem p) z | z in enum_val @^-1: x].
proof: Proof. move/subsetP => Hxp. apply/setP=> y. symmetry. apply/imsetP. case: ifPn => Hyx. rewrite -(@can2_in_imset_pre _ _ (enum_rank_in (Hxp _ Hyx))). esplit; first exact/imset_f/Hyx. by rewrite enum_rankK_in // Hxp. by move=> z Hz; exact: (enum_rankK_in _ (Hxp _ Hz)). by move=> z Hz; rewrite enum_valK_in. move=> [z Hz Hzy]. rewrite /preimset inE in Hz. by rewrite Hzy Hz in Hyx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist