proposition: Lemma morphim_class x A : x \in D -> A \subset D -> f @* (x ^: A) = f x ^: f @* A.
proof: Proof. move=> Dx sAD; rewrite !morphimEsub ?class_subG // /class -!imset_comp. by apply: eq_in_imset => y Ay /=; rewrite morphJ // (subsetP sAD). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)