proposition: Lemma char_from_quotient (gT : finGroupType) (G H K : {group gT}) : H <| K -> H \char G -> K / H \char G / H -> K \char G.
proof: Proof. case/andP=> sHK nHK chHG. have nsHG := char_normal chHG; have [sHG nHG] := andP nsHG. case/charP; rewrite quotientSGK // => sKG /= chKG. apply/charP; split=> // f injf Gf; apply/morphim_fixP => //. rewrite -(quotientSGK _ sHK); last by rewrite -morphimIim Gf subIset ?nHG. have{chHG} Hf: f @* H = H by case/charP: chHG => _; apply. set q := quotm_morphism f nsHG; have{injf}: 'injm q by apply: injm_quotm. have: q @* _ = _ := morphim_quotm _ _ _; move: q; rewrite Hf => q im_q injq. by rewrite -im_q chKG // im_q Gf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)