proposition: Lemma eq_in_pHall pi rho G H : {in \pi(G), pi =i rho} -> pi.-Hall(G) H = rho.-Hall(G) H.
proof: Proof. move=> eq_pi_rho; apply: andb_id2l => sHG. congr (_ && _); apply: eq_in_pnat => p piHp. by apply: eq_pi_rho; apply: (piSg sHG). by congr (~~ _); apply: eq_pi_rho; apply: (pi_of_dvd (dvdn_indexg G H)). 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)