proposition: Lemma first_isom_loc : {g : {morphism H / 'ker_H f >-> rT} | 'injm g & forall A : {set aT}, A \subset H -> g @* (A / 'ker_H f) = f @* A}.
proof: Proof. case: (first_isom (restrm_morphism sHG f)). rewrite ker_restrm => g injg im_g; exists g => // A sAH. by rewrite im_g morphim_restrm (setIidPr sAH). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)