proposition: Lemma aksP n : aks n = prime n.
proof: Proof. case: n => //; case => // m. have : 1 < m.+2 by []; move: m.+2 => {m}n n_gt1; rewrite /aks; set l := up_log 2 n. case: power_free (@power_freeP n) (@power_freePn n) => [H _ | _ /(_ isT) [m [k k_gt1 ->]]]; last first. have k_gt0 : 0 < k by apply: ltnW. apply/sym_equal/idP => /primePn[]. case: m => [|[|m]]; first by left; rewrite exp0n. by left; rewrite exp1n. right; exists m.+2; first by rewrite /= -{1}[m.+2]expn1 ltn_exp2l. by apply: dvdn_exp. case: aks_param (aks_paramP n) => // [m /(_ n_gt1) [m_gt1 _ mDn nP]|k [kB nP kLl kCm lLo]]. move: nP; case: eqP => [->|HD] nP; apply/sym_equal/idP. apply/primeP; split => // [] [|[|d]] //. by rewrite dvd0n; case: (m) m_gt1. move=> dDm /=; case: eqP => // d2Dm. suff /nP/negP[]/= : 1 < d.+2 < m by []. by have := dvdn_leq (ltnW m_gt1) dDm; rewrite leq_eqVlt => /orP[/eqP|]. apply/negP/primePn; right; exists m => //. rewrite m_gt1 /=. have := dvdn_leq (ltnW n_gt1) mDn; rewrite leq_eqVlt => /orP[/eqP|] // mEn. by case: HD. have k_gt1 : 1 < k by case/andP: kB. case: fpoly_intro_range (fpoly_intro_rangeP l k_gt1 n_gt1); last first. by case: prime. case: (boolP (prime n)) => // /negP nNP. have pkn_gt1 : 1 < order_modn k n. apply: leq_trans lLo. apply: leq_trans (_ : up_log 2 4 ^ 2 <= _) => //. rewrite leq_exp2r // leq_up_log //. by case: (n) n_gt1 nNP => // [] [|[|[|]]]. have [p [pDn pP pO]] := order_gt1_prime n_gt1 pkn_gt1. move/(inZpm_poly_intro_range n_gt1 pP pDn (ltnW k_gt1)) => Hp. suff : is_power n p. move/eqP => nE. by case: nNP; rewrite nE (H _ _ isT nE) expn1. apply: (@main_aks p n k) => //. split => //=; try by apply: ltnW. move=> p1; rewrite inE => /andP[p1P]. rewrite -(dvdn_charf (char_Fp _)) // dvdn_prime2 ?pdiv_prime // => /eqP<-. split=> //. case: leqP => // pLk. by have /nP/negP[] : 1 < p <= k by rewrite prime_gt1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound