proposition: Lemma gen_expgs A : {n | <<A>> = (1 |: A) ^+ n}.
proof: Proof. set B := (1 |: A); pose N := #|gT|. have BsubG n : B ^+ n \subset <<A>>. by elim: n => [|n IHn]; rewrite ?expgS ?mul_subG ?subUset ?sub1G ?subset_gen. have B_1 n : 1 \in B ^+ n. by elim: n => [|n IHn]; rewrite ?set11 // expgS mulUg mul1g inE IHn. case: (pickP (fun i : 'I_N => B ^+ i.+1 \subset B ^+ i)) => [n fixBn | no_fix]. exists n; apply/eqP; rewrite eqEsubset BsubG andbT. rewrite -[B ^+ n]gen_set_id ?genS ?subsetUr //. by apply: subset_trans fixBn; rewrite expgS mulUg subsetU ?mulg_subl ?orbT. rewrite /group_set B_1 /=. elim: {2}(n : nat) => [|m IHm]; first by rewrite mulg1. by apply: subset_trans fixBn; rewrite !expgSr mulgA mulSg. suffices: N < #|B ^+ N| by rewrite ltnNge max_card. have [] := ubnPgeq N; elim=> [|n IHn] lt_nN; first by rewrite cards1. apply: leq_ltn_trans (IHn (ltnW lt_nN)) (proper_card _). by rewrite /proper (no_fix (Ordinal lt_nN)) expgS mulUg mul1g subsetUl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)