proposition: Lemma gen_subG A G : (<<A>> \subset G) = (A \subset G).
proof: Proof. apply/idP/idP=> [|sAG]; first exact: subset_trans (subset_gen A). by apply/subsetP=> x /generatedP; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)