proposition: Lemma inZpm_poly_intro_range k s : 0 < k -> poly_intro_range (GRing.Ring.clone _ 'Z_n) k n s -> poly_intro_range (GRing.Ring.clone _ 'F_p) k n s.
proof: Proof. move=> k_gt0. have xnZM := monic_Xn_sub_1 (GRing.Ring.clone _ 'Z_n) k_gt0. have xnFM := monic_Xn_sub_1 (GRing.Ring.clone _ 'F_p) k_gt0. have p_gt1 : 1 < pdiv n by apply/prime_gt1/pdiv_prime. move=> Hr c cB; apply/eqP; rewrite eqp_rmodp_dvd //. have /eqP := Hr c cB; rewrite eqp_rmodp_dvd //. case /(rdvdpP xnZM) => /= p1 pE; apply/(rdvdpP xnFM). exists (map_poly inZpm p1). rewrite (_ : 'X^k - 1 = map_poly inZpm ('X^k - 1)); last first. by rewrite rmorphB rmorph1 /= (map_polyXn inZpm). have cE : inZp (c%:R : 'Z_n) = c%:R :> 'F_p. by apply/val_eqP; rewrite /= !Zp_nat /= Fp_cast // Zp_cast // modn_dvdm // pDn. rewrite -rmorphM -pE !(rmorphB, rmorphXn, rmorphD) /=. by rewrite (map_polyX inZpm) (map_polyC inZpm) /= cE. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound