proposition: Lemma injm_normal A B : A \subset D -> B \subset D -> (f @* A <| f @* B) = (A <| B).
proof: Proof. by move=> sAD sBD; rewrite /normal injmSK ?injm_norms. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)