proposition: Lemma morphpreJ R x : x \in D -> f @*^-1 (R :^ f x) = f @*^-1 R :^ x.
proof: Proof. move=> Dx; apply/setP=> y; rewrite conjIg !inE conjGid // !mem_conjg inE. by case Dy: (y \in D); rewrite // morphJ ?(morphV, groupV). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)