proposition: Lemma dvdn_orderC x n : (#[x]%C %| n)%N = (x ^+ n == 1).
proof: Proof. apply/idP/eqP=> [|x_n_1]; first by apply: expr_dvd; apply: exp_orderC. have [-> | n_gt0] := posnP n; first by rewrite dvdn0. have [m prim_x m_dv_n] := prim_order_exists n_gt0 x_n_1. have{n_gt0} m_gt0 := dvdn_gt0 n_gt0 m_dv_n; congr (_ %| n)%N: m_dv_n. pose p := minCpoly x; have Dp: p = cyclotomic x m := minCpoly_cyclotomic prim_x. rewrite /orderC; case: pickP => /= [k /eqP Dp_k | no_k]; last first. suffices lt_m_2p: (m < 2 * size p ^ 2)%N. have /eqP[] := no_k (Ordinal lt_m_2p). by rewrite /= -/p Dp -Cintr_Cyclotomic. rewrite Dp size_cyclotomic (sqrnD 1) addnAC mulnDr -add1n leq_add //. suffices: (m <= \prod_(q <- primes m | q == 2) q * totient m ^ 2)%N. have [m_even | m_odd] := boolP (2%N \in primes m). by rewrite -big_filter filter_pred1_uniq ?primes_uniq // big_seq1. by rewrite big_hasC ?has_pred1 // => /leq_trans-> //; apply: leq_addl. rewrite big_mkcond totientE // -mulnn -!big_split /=. rewrite {1}[m]prod_prime_decomp // prime_decompE big_map /= !big_seq. elim/big_ind2: _ => // [n1 m1 n2 m2 | q]; first exact: leq_mul. rewrite mem_primes => /and3P[q_pr _ q_dv_m]. rewrite lognE q_pr m_gt0 q_dv_m /=; move: (logn q _) => k. rewrite !mulnA expnS leq_mul //. case: (ltngtP q 2) (prime_gt1 q_pr) => // [q_gt2|->] _. rewrite mul1n mulnAC mulnn -{1}[q]muln1 leq_mul ?expn_gt0 ?prime_gt0 //. by rewrite -(subnKC q_gt2) (ltn_exp2l 1). by rewrite !muln1 -expnS (ltn_exp2l 0). have k_prim_x: k.-primitive_root x. have k_gt0: (0 < k)%N. rewrite lt0n; apply: contraTneq (size_minCpoly x) => k0. by rewrite Dp_k k0 Cyclotomic0 rmorph1 size_poly1. have [z prim_z] := C_prim_root_exists k_gt0. rewrite -(root_cyclotomic prim_z) -Cintr_Cyclotomic //. by rewrite -Dp_k root_minCpoly. apply/eqP; rewrite eqn_dvd !(@prim_order_dvd _ _ x) //. by rewrite !prim_expr_order ?eqxx. 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)