proposition: Lemma coprime_sdprod_Hall_l G K H : K ><| H = G -> coprime #|K| #|H| = Hall G K.
proof: Proof. case/sdprod_context=> /andP[sKG _] _ defG _ tiKH. by rewrite /Hall sKG -divgS // -defG TI_cardMg ?mulKn. 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)