proposition: Lemma poly_intro_range_auxP n pn k c r : 1 < k -> 1 < n -> pn = Pos.of_nat n -> if poly_intro_range_aux n pn k c r then forall c1, c <= c1 < c + r -> rmodp (('X + (c1%:R)%:P) ^+ n) ('X^k - 1) = rmodp ('X^n + (c1%:R)%:P) ('X^k - 1) :> {poly 'Z_n} else ~ prime n.
proof: Proof. move=> k_gt1 n_gt1 pnE. have k_gt0 : 0 < k by apply: leq_trans k_gt1. elim: r c => /= [c c1|r IH c]; first by rewrite addn0; case: ltngtP. rewrite poly_modnp_eq // poly_modnp_pow ?size_modnp_add //. rewrite !poly_modnp_add // !poly_modnp_Xn // poly_modnp_const // pnE. rewrite Pnat.Nat2Pos.id_max max_r; last by apply/leP/ltnW. rewrite expr1 [rmodp 'X _]rmodp_small; last first. by rewrite size_polyX size_Xn_sub_1. case: eqP => mE; last first. move=> nP; case: mE. have xnM := monic_Xn_sub_1 (GRing.Ring.clone _ 'Z_n) k_gt0. rewrite exprDn_char /=; last first. rewrite pnatE // char_poly /= inE nP /=. apply/eqP/val_eqP=> /=. by rewrite val_Zp_nat // modnn. rewrite rmodpD //; congr (_ + _). rewrite rmodp_small //; last first. apply: leq_ltn_trans (size_exp_leq _ _) _. rewrite size_polyC size_Xn_sub_1 //. by case: (_ != _). rewrite -rmorphXn; congr (_ %:P). pose i := inZpm n_gt1 nP (dvdnn n). suff : i (c%:R ^+ n) = i c%:R. move/val_eqP/eqP=> /=; rewrite Fp_cast //. rewrite !modn_small //; try by rewrite -[n]Zp_cast ?prime_gt1. by move=> H; apply/val_eqP/eqP. rewrite rmorphXn rmorph_nat. by apply: fin_little_fermat c (char_Fp nP). rewrite -pnE. case: poly_intro_range_aux (IH c.+1) => // H c1. rewrite addnS ltnS [c <= _]leq_eqVlt => /andP[/orP[/eqP<-//|cLc1] c1Lcr]. rewrite rmodpD ?monic_Xn_sub_1 //. rewrite [X in _ = _ + X]rmodp_small // size_Xn_sub_1 // size_polyC. by case: eqP. by apply: H; rewrite cLc1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound