proposition: Lemma morphim_pprod : pprod K H = G -> pprod (f @* K) (f @* H) = f @* G.
proof: Proof. case/pprodP=> _ defG mKH; rewrite pprodE ?morphim_norms //. by rewrite -morphimMl ?(subset_trans _ sGD) -?defG // mulG_subl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)