proposition: Lemma order_gt1_prime k n : 1 < n -> 1 < order_modn k n -> exists p : nat, [/\ (p %| n), prime p & 1 < order_modn k p]%nat.
proof: Proof. move=> n_gt1 o_gt1. have k_gt1 := order_modn_gt1 o_gt1. have [/allP Ho|/allPn] := boolP (all (fun i => order_modn k i <= 1) (primes n)); last first. case=> p; rewrite mem_primes -ltnNge => /and3P[pP _ pDn] pO. by exists p. have B1 : 0 < 1 < order_modn k n by []. have [_ _ /(_ _ B1)/eqP[]] := order_modnP k_gt1 (order_modn_coprime o_gt1). rewrite expn1 [n]prod_prime_decomp 1?ltnW // prime_decompE. rewrite big_seq_cond -modn_prodm big1 // => [] [p r]. rewrite andbT => /mapP[q qP [-> ->]] /=. have oL1 := Ho _ qP. have kCq : coprime k q. apply: coprime_dvdr (order_modn_coprime o_gt1). by rewrite mem_primes in qP; case/and3P: qP. have [H1 H2 _] := order_modnP k_gt1 kCq. rewrite -modnXm -[q]expn1 -{1}(_ : order_modn k q = 1%nat). by rewrite H2 modnXm exp1n modn_small. by apply/eqP; rewrite eqn_leq oL1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)