proposition: Lemma seq_index_enum_card A : forall s (E : {set A}) a, s =i enum E -> uniq s -> a \in E -> index a s < #| E |.
proof: Proof. elim => [E a _ _ aE| h t IH E a htE uniqht aE /=]. exact: enum_rank_subproof aE. case: ifPn => [_|hi]; first by rewrite card_gt0; apply/set0Pn; exists a. apply (@leq_ltn_trans #|E :\ h|); last first. by rewrite (cardsD1 h E) -mem_enum -htE mem_head add1n. apply IH. - move=> j; case/boolP : (j \in enum (E :\ h)). + rewrite mem_enum in_setD1 => /andP[/negbTE H]. by rewrite -mem_enum -htE in_cons H. + rewrite mem_enum in_setD1 negb_and negbK => /orP[/eqP ->{j}|]. - by move: uniqht => /= /andP[/negbTE]. - by rewrite -mem_enum -htE inE negb_or => /andP[_ /negbTE]. - move: uniqht; by case/andP. - apply/setD1P; by rewrite eq_sym. Qed.
imports: mathcomp(all_ssreflect fingroup perm)