proposition: Lemma act_g_morph : forall k x y, act_g k (x * y) = act_g (act_g k x) y.
proof: Proof. by move=> k x y; apply/ffunP=> a; rewrite !ffunE invMg permE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)