proposition: Lemma setact_is_action : is_action D to^*.
proof: Proof. split=> [a R S eqRS | a b Da Db S]; last first. by rewrite /setact /= -imset_comp; apply: eq_imset => x; apply: actMin. apply/setP=> x; apply/idP/idP=> /(mem_setact a). by rewrite eqRS => /imsetP[y Sy /act_inj->]. by rewrite -eqRS => /imsetP[y Sy /act_inj->]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)