proposition: Lemma classes_morphim A : A \subset D -> classes (f @* A) = [set f @* xA | xA in classes A].
proof: Proof. move=> sAD; rewrite morphimEsub // /classes -!imset_comp. apply: eq_in_imset => x /(subsetP sAD) Dx /=. by rewrite morphim_class ?morphimEsub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)