proposition: Lemma sdprod_modr A B G H : A ><| B = G -> B \subset H -> (H :&: A) ><| B = H :&: G.
proof: Proof. case/sdprodP=> {A B}[[A B -> ->]] <- nAB tiAB sAH. rewrite -group_modr ?sdprodE ?normsI // ?normsG //. by rewrite -setIA tiAB (setIidPr _) ?sub1G. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)