proposition: Lemma int_eqAmod_prime_prim n : prime p -> n \in Cint -> (n == 0 %[mod e])%A -> (p %| n)%C.
proof: Proof. move=> p_pr Zn; rewrite /eqAmod unfold_in subr0. have p_gt0 := prime_gt0 p_pr. case: ifPn => [_ /eqP->// | nz_e e_dv_n]. suffices: (n ^+ p.-1 == 0 %[mod p])%A. rewrite eqAmod0_rat ?rpredX ?rpred_nat 1?rpred_Cint // !dvdC_int ?rpredX //. by rewrite floorCX // abszX Euclid_dvdX // => /andP[]. rewrite /eqAmod subr0 unfold_in pnatr_eq0 eqn0Ngt p_gt0 /=. pose F := \prod_(1 <= i < p) ('X - (eps ^+ i)%:P). have defF: F = \sum_(i < p) 'X^i. apply: (mulfI (monic_neq0 (monicXsubC 1))); rewrite -subrX1. by rewrite -(factor_Xn_sub_1 pr_eps) big_ltn. have{defF} <-: F.[1] = p :> Algebraics.divisor. rewrite -[p]card_ord -[rhs in _ = rhs]sumr_const defF horner_sum. by apply: eq_bigr => i _; rewrite hornerXn expr1n. rewrite -[p.-1]card_ord {F}horner_prod big_add1 big_mkord -prodfV. rewrite -prodr_const -big_split rpred_prod //= => k _; rewrite !hornerE. rewrite -[n](divfK nz_e) -[_ * _ / _]mulrA rpredM {e_dv_n}//. have p'k: ~~ (p %| k.+1)%N by rewrite gtnNdvd // -{2}(prednK p_gt0) ltnS. have [r {1}->]: exists r, eps = eps ^+ k.+1 ^+ r. have [q _ /dvdnP[r Dr]] := Bezoutl p (ltn0Sn k); exists r; apply/esym/eqP. rewrite -exprM (eq_prim_root_expr pr_eps _ 1) mulnC -Dr addnC gcdnC. by rewrite -prime_coprime // in p'k; rewrite (eqnP p'k) modnMDl. rewrite -[1 - _]opprB subrX1 -mulNr opprB mulrC. rewrite mulKf; last by rewrite subr_eq0 eq_sym -(prim_order_dvd pr_eps). by apply: rpred_sum => // i _; rewrite !rpredX ?(Aint_prim_root pr_eps). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)