proposition: Lemma norm_joinEl G H : G \subset 'N(H) -> G <*> H = G * H.
proof: Proof. by move/normC/comm_joingE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)