proposition: Lemma sdprod_isom G A B : A ><| B = G -> {nAB : B \subset 'N(A) | isom B (G / A) (restrm nAB (coset A))}.
proof: Proof. case/sdprodP=> [[K H -> ->] <- nKH tiKH]. by exists nKH; rewrite quotientMidl quotient_isom. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)