proposition: Lemma dprodA : associative dprod.
proof: Proof. move=> A B C; case A1: (A == 1); first by rewrite (eqP A1) !dprod1g. case B1: (B == 1); first by rewrite (eqP B1) dprod1g dprodg1. case C1: (C == 1); first by rewrite (eqP C1) !dprodg1. rewrite /dprod (fun_if (cprod A)) (fun_if (cprod^~ C)) -cprodA. rewrite -(cprodC set0) !cprod0g cprod_ntriv ?B1 ?{}C1 //. case: and3P B1 => [[] | _ _]; last by rewrite cprodC cprod0g !if_same. case/isgroupP=> H ->; case/isgroupP=> K -> {B C}; move/cent_joinEr=> eHK H1. rewrite cprod_ntriv ?trivMg ?{}A1 ?{}H1 // mulG_subG. case: and4P => [[] | _]; last by rewrite !if_same. case/isgroupP=> G ->{A} _ cGH _; rewrite cprodEY // -eHK. case trGH: (G :&: H \subset _); case trHK: (H :&: K \subset _); last first. - by rewrite !if_same. - rewrite if_same; case: ifP => // trG_HK; case/negP: trGH. by apply: subset_trans trG_HK; rewrite setIS ?joing_subl. - rewrite if_same; case: ifP => // trGH_K; case/negP: trHK. by apply: subset_trans trGH_K; rewrite setSI ?joing_subr. do 2![case: ifP] => // trGH_K trG_HK; [case/negP: trGH_K | case/negP: trG_HK]. apply: subset_trans trHK; rewrite subsetI subsetIr -{2}(mulg1 H) -mulGS. rewrite setIC group_modl ?joing_subr //= cent_joinEr // -eHK. by rewrite -group_modr ?joing_subl //= setIC -(normC (sub1G _)) mulSg. apply: subset_trans trGH; rewrite subsetI subsetIl -{2}(mul1g H) -mulSG. rewrite setIC group_modr ?joing_subl //= eHK -(cent_joinEr cGH). by rewrite -group_modl ?joing_subr //= setIC (normC (sub1G _)) mulgS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)