proposition: Fact actr_is_groupAction : is_groupAction setT 'M.
proof: Proof. move=> a Na /[1!inE]; apply/andP; split; first by apply/subsetP=> u _ /[1!inE]. by apply/morphicP=> u v _ _; rewrite !permE /= actAr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)