proposition: Lemma exp_orderC x : x ^+ #[x]%C = 1.
proof: Proof. rewrite /orderC; case: pickP => //= [] [n _] /= /eqP Dp. have n_gt0: (0 < n)%N. rewrite lt0n; apply: contraTneq (size_minCpoly x) => n0. by rewrite Dp n0 Cyclotomic0 rmorph1 size_poly1. have [z prim_z] := C_prim_root_exists n_gt0. rewrite prim_expr_order // -(root_cyclotomic prim_z). by rewrite -Cintr_Cyclotomic // -Dp root_minCpoly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)