proposition: Lemma ker_norm : D \subset 'N('ker f).
proof: Proof. apply/subsetP=> x Dx /[1!inE]; apply/subsetP=> _ /imsetP[y Ky ->]. by rewrite !inE groupJ ?morphJ // ?dom_ker //= mker ?conj1g. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)