proposition: Lemma sdprod_Hall G K H : K ><| H = G -> Hall G K = Hall G H.
proof: Proof. case/sdprod_context=> /andP[sKG _] sHG defG _ tiKH. by rewrite /Hall sKG sHG -!divgS // -defG TI_cardMg // coprime_sym mulKn ?mulnK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)