proposition: Lemma mulgmP H1 H2 G : reflect (H1 \x H2 = G) (misom (setX H1 H2) G mulgm).
proof: Proof. apply: (iffP misomP) => [[pM /isomP[injf /= <-]] | ]. have /dprodP[_ /= defX cH12] := setX_dprod H1 H2. rewrite -{4}defX {}defX => /(congr1 (fun A => morphm pM @* A)). move/(morphimS (morphm_morphism pM)): cH12 => /=. have sH1H: setX H1 1 \subset setX H1 H2 by rewrite setXS ?sub1G. have sH2H: setX 1 H2 \subset setX H1 H2 by rewrite setXS ?sub1G. rewrite morphim1 injm_cent ?injmI //= subsetI => /andP[_]. by rewrite !morphimEsub //= !imset_mulgm mulg1 mul1g; apply: dprodE. case/dprodP=> _ defG cH12 trH12. have fM: morphic (setX H1 H2) mulgm. apply/morphicP=> [[x1 x2] [y1 y2] /setXP[_ Hx2] /setXP[Hy1 _]]. by rewrite /= mulgA -(mulgA x1) -(centsP cH12 x2) ?mulgA. exists fM; apply/isomP; split; last by rewrite morphimEsub //= imset_mulgm. apply/subsetP=> [[x1 x2]]; rewrite !inE /= andbC -eq_invg_mul. case: eqP => //= <-; rewrite groupV -in_setI trH12 => /set1P->. by rewrite invg1 eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)