proposition: Lemma morphim_cprod : K \* H = G -> f @* K \* f @* H = f @* G.
proof: Proof. case/cprodP=> _ defG cKH; rewrite /cprod morphim_cents // morphim_pprod //. by rewrite pprodE // cents_norm // centsC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)