proposition: Lemma morphpre_quotm Abar : quotm @*^-1 (Abar / f @* H) = f @*^-1 Abar / H.
proof: Proof. rewrite morphpre_factm morphpre_restrm morphpre_comp /=. rewrite morphpreIdom -[Abar / _]quotientInorm quotientK ?subsetIr //=. rewrite morphpreMl ?morphimS // morphimK // [_ * H]normC ?subIset ?nHG //. rewrite -quotientE -mulgA quotientMidl /= setIC -morphpreIim setIA. by rewrite (setIidPl nfHfG) morphpreIim -morphpreMl ?sub1G ?mul1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)