proposition: Lemma comp_is_action : is_action (f @*^-1 D) comp_act.
proof: Proof. split=> [e | x e1 e2]; first exact: act_inj. move=> /morphpreP[Be1 Dfe1] /morphpreP[Be2 Dfe2]. by rewrite /comp_act morphM ?actMin. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)