proposition: Lemma der1_subG G : [~: G, G] \subset G.
proof: Proof. by rewrite gen_subG; apply/subsetP=> _ /imset2P[x y Gx Gy ->]; apply: groupR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)