proposition: Lemma reindex_astabs a F : a \in 'N(S | to) -> \big[op/idx]_(i in S) F i = \big[op/idx]_(i in S) F (to i a).
proof: Proof. move=> nSa; rewrite (reindex_inj (act_inj a)); apply: eq_bigl => x. exact: astabs_act. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)