proposition: Lemma sdprod_normal_complP G K H : K <| G -> reflect (K ><| H = G) (K \in [complements to H in G]).
proof: Proof. case/andP=> _ nKG; rewrite complgC. apply: (iffP idP); [case/complP=> tiKH mulKH | exact: sdprod_compl]. by rewrite sdprodE ?(subset_trans _ nKG) // -mulKH mulG_subr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)