proposition: Lemma dprodYP K H : reflect (K \x H = K <*> H) (H \subset 'C(K) :\: K^#).
proof: Proof. rewrite subsetD -setI_eq0 setIDA setD_eq0 setIC subG1 /=. by apply: (iffP andP) => [[cKH /eqP/dprodEY->] | /dprodP[_ _ -> ->]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)