proposition: Lemma dprodP A B G : A \x B = G -> [/\ are_groups A B, A * B = G, B \subset 'C(A) & A :&: B = 1].
proof: Proof. rewrite /dprod; case: ifP => trAB; last by case/group_not0. by case/cprodP=> gAB; split=> //; case: gAB trAB => ? ? -> -> /trivgP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)