proposition: Lemma cprodP A B G : A \* B = G -> [/\ are_groups A B, A * B = G & B \subset 'C(A)].
proof: Proof. by rewrite /cprod; case: ifP => [cAB /pprodP[] | _ /group_not0[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)