proposition: Lemma enum_cons (s : {set T}) (x : T) : ohead (enum s) = Some x -> enum s = x :: enum (s :\ x).
proof: Proof. rewrite /enum_mem -enumT. elim: (enum T) (enum_uniq T) => //= y l ih /andP [yl ul]. case: ifP => /= [ys [<-]|yNs oxs]. rewrite !inE eqxx /=; congr cons; apply eq_in_filter => z zl. by rewrite !inE; case: eqP zl yl => // -> ->. by rewrite ih //= !inE yNs andbF. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist