proposition: Lemma first_isog_loc : (H / 'ker_H f) \isog (f @* H).
proof: Proof. by case: first_isom_loc => g injg im_g; apply/isogP; exists g; rewrite ?im_g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)