proposition: Lemma cprodA : associative cprod.
proof: Proof. move=> A B C; case A1: (A == 1); first by rewrite (eqP A1) !cprod1g. case B1: (B == 1); first by rewrite (eqP B1) cprod1g cprodg1. case C1: (C == 1); first by rewrite (eqP C1) !cprodg1. rewrite !(triv_cprod, cprod_ntriv) ?{}A1 ?{}B1 ?{}C1 //. case: isgroupP => [[G ->{A}] | _]; last by rewrite group0. case: (isgroupP B) => [[H ->{B}] | _]; last by rewrite group0. case: (isgroupP C) => [[K ->{C}] | _]; last by rewrite group0 !andbF. case cGH: (H \subset 'C(G)); case cHK: (K \subset 'C(H)); last first. - by rewrite group0. - by rewrite group0 /= mulG_subG cGH andbF. - by rewrite group0 /= centM subsetI cHK !andbF. rewrite /= mulgA mulG_subG centM subsetI cGH cHK andbT -(cent_joinEr cHK). by rewrite -(cent_joinEr cGH) !groupP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)