proposition: Lemma pprodE K H : H \subset 'N(K) -> pprod K H = K * H.
proof: Proof. move=> nKH; rewrite /pprod nKH !groupP /=. by do 2?case: eqP => [-> | _]; rewrite ?mulg1 ?mul1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)