proposition: Lemma nclasses_injm A : A \subset D -> #|classes (f @* A)| = #|classes A|.
proof: Proof. move=> sAD; rewrite classes_morphim // card_in_imset //. move=> _ _ /imsetP[x Ax ->] /imsetP[y Ay ->]. by apply: injm_morphim_inj; rewrite // class_subG ?(subsetP sAD). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)