proposition: Lemma first_isom (G : {group aT}) (f : {morphism G >-> rT}) : {g : {morphism G / 'ker f >-> rT} | 'injm g & forall A : {set aT}, g @* (A / 'ker f) = f @* A}.
proof: Proof. have nkG := ker_norm f. have skk: 'ker (coset ('ker f)) \subset 'ker f by rewrite ker_coset. exists (factm_morphism skk nkG) => /=; last exact: morphim_factm. by rewrite ker_factm -quotientE trivg_quotient. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)