proposition: Lemma pprodP A B G : pprod A B = G -> [/\ are_groups A B, A * B = G & B \subset 'N(A)].
proof: Proof. have Gnot0 := @group_not0 G; rewrite /pprod; do 2?case: eqP => [-> ->| _]. - by rewrite mul1g norms1; split; first exists 1%G G. - by rewrite mulg1 sub1G; split; first exists G 1%G. by case: and3P => // [[gA gB ->]]; split; first exists (Group gA) (Group gB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)