proposition: Lemma mulG_subG G H K : (G * H \subset K) = (G \subset K) && (H \subset K).
proof: Proof. by rewrite -gen_subG genM_join join_subG. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)