proposition: Lemma cprod_modl A B G H : A \* B = G -> A \subset H -> A \* (B :&: H) = G :&: H.
proof: Proof. case/cprodP=> [[U V -> -> {A B}]] defG cUV sUH. by rewrite cprodE; [rewrite group_modl ?defG | rewrite subIset ?cUV]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)