proposition: Lemma gX_order : #[gX]%g = (#|qT|).-1.
proof: Proof. have /primitive_polyP[Hp1 Hp2 Hp3] := Hh. set n := _.-1 in Hp2 Hp3 *. have n_gt0 : 0 < n by rewrite ltn_predRL card_qfpoly_gt1. have [hM hI] := primitive_mi. have gX_neq1 : gX != 1%g. apply/eqP/val_eqP/eqP/val_eqP=> /=. rewrite [X in X != _]qpolyXE /= //. by apply/eqP=> Hx1; have := @size_polyX F; rewrite Hx1 size_poly1. have Hx : (gX ^+ n)%g = 1%g by apply/eqP; rewrite -dvdp_order. have Hf i : 0 < i < n -> (gX ^+ i != 1)%g by rewrite -dvdp_order => /Hp3. have o_gt0 : 0 < #[gX]%g by rewrite order_gt0. have : n <= #[gX]%g. rewrite leqNgt; apply/negP=> oLx. have /Hf/eqP[] : 0 < #[gX]%g < n by rewrite o_gt0. by rewrite expg_order. case: ltngtP => nLo _ //. have: uniq (path.traject (mulg gX) 1%g #[gX]%g). by apply/card_uniqP; rewrite path.size_traject -(eq_card (cycle_traject gX)). case: #[gX]%g o_gt0 nLo => //= n1 _ nLn1 /andP[/negP[]]. apply/path.trajectP; exists n.-1; first by rewrite prednK. rewrite -iterSr prednK // -[LHS]Hx. by elim: (n) => //= n2 <-; rewrite expgS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(div bigop binomial finset finfun ssralg countalg finalg) mathcomp(poly polydiv qpoly perm fingroup falgebra fieldext finfield galois) mathcomp(finalg zmodp matrix vector)