proposition: Lemma enum_val_bij_on : x \subset p -> x != set0 -> {on x, bijective (@enum_val _ (mem p))}.
proof: Proof. move=> /subsetP Hxp. case: (set_0Vmem x) => [->|[z Hz] _]. by rewrite eqxx. by apply (subon_bij Hxp), (enum_val_bij_in (Hxp _ Hz)). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist