proposition: Lemma comp_is_groupAction : is_groupAction R (comp_action to f).
proof: Proof. move=> a /morphpreP[Ba Dfa]; apply: etrans (actperm_Aut to Dfa). by congr (_ \in Aut R); apply/permP=> x; rewrite !actpermE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)