proposition: Lemma injm_dprod : 'injm f -> K \x H = G -> f @* K \x f @* H = f @* G.
proof: Proof. move=> inj_f; case/dprodP=> _ defG cHK tiKH. by rewrite /dprod -injmI // tiKH morphim1 subxx morphim_cprod // cprodE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)