proposition: Lemma qX_exp_inj i j : i < #|qT|.-1 -> j < #|qT|.-1 -> 'qX ^+ i = 'qX ^+ j :> qT -> i = j.
proof: Proof. wlog iLj : i j / (i <= j)%N => [Hw|] iL jL Hqx. case: (ltngtP i j)=> // /ltnW iLj; first by apply: Hw. by apply/sym_equal/Hw. suff ji_eq0 : (j - i = 0)%N by rewrite -(subnK iLj) ji_eq0. case: ((j - i)%N =P 0%N) => // /eqP ji_neq0. have : j - i < #|qT|.-1 by apply: leq_ltn_trans (leq_subr _ _) jL. rewrite ltnNge => /negP[]. apply: dvdn_leq; first by rewrite lt0n. have HqXi : 'qX ^+ i != 0 :> qT by rewrite expf_eq0 (negPf qX_neq0) andbF. by apply/qX_order_dvd/(mulIf HqXi); rewrite mul1r -exprD subnK. 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)