proposition: Lemma sdprodE K H : H \subset 'N(K) -> K :&: H = 1 -> K ><| H = K * H.
proof: Proof. by move=> nKH tiKH; rewrite /sdprod tiKH subxx pprodE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)