proposition: Lemma dvdp_order n : (h %| 'X^n - 1) = (gX ^+ n == 1)%g.
proof: Proof. have [hM hI] := primitive_mi. have eqr_add2r (r : ringType) (a b c : r) : (a + c == b + c) = (a == b). by apply/eqP/eqP => [H|->//]; rewrite -(addrK c a) H addrK. rewrite -val_eqE /= val_unitX /= -val_eqE /=. rewrite (poly_of_qpolyX) qpolyXE // mk_monicE //. rewrite -[in RHS](subrK 1 'X^n) rmodpD //. rewrite [rmodp 1 h]rmodp_small ?size_poly1 //. rewrite -[1%:P]add0r polyC1 /= eqr_add2r. by rewrite dvdpE /=; apply/rmodp_eq0P/eqP. 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)