proposition: Lemma gX_all : <[gX]>%g = [set: {unit qT}]%G.
proof: Proof. apply/eqP; rewrite eqEcard; apply/andP; split. by apply/subsetP=> i; rewrite inE. rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite -orderE gX_order card_qfpoly -[in RHS](mk_monicE primitive_mi). rewrite -card_qpoly -(cardC1 (0 : {poly %/ h with primitive_mi})). rewrite cardsT card_sub. by apply: eq_card => x; rewrite [LHS]unitfE. 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)