proposition: Lemma subact_is_action : is_action subact_dom subact.
proof: Proof. split=> [a u v eq_uv | u a b Na Nb]; apply: val_inj. move/(congr1 val): eq_uv; rewrite !val_subact. by case: (a \in _); first move/act_inj. have Da := astabs_dom Na; have Db := astabs_dom Nb. by rewrite !val_subact Na Nb groupM ?actMin. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)