proposition: Lemma genD1 A x : x \in <<A :\ x>> -> <<A :\ x>> = <<A>>.
proof: Proof. move=> gA'x; apply/eqP; rewrite eqEsubset genS; last by rewrite subsetDl. rewrite gen_subG; apply/subsetP=> y Ay. by case: (y =P x) => [-> //|]; move/eqP=> nyx; rewrite mem_gen // !inE nyx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)