proposition: Lemma sdprodP A B G : A ><| B = G -> [/\ are_groups A B, A * B = G, B \subset 'N(A) & A :&: B = 1].
proof: Proof. rewrite /sdprod; case: ifP => [trAB | _ /group_not0[] //]. case/pprodP=> gAB defG nBA; split=> {defG nBA}//. by case: gAB trAB => H K -> -> /trivgP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)