proposition: Lemma fpoly_intro_rangeP n k l : 1 < k -> 1 < n -> if fpoly_intro_range n k l then poly_intro_range (GRing.Ring.clone _ 'Z_n) k n (sqrtn (totient k) * l) else ~ prime n.
proof: Proof. move=> k_gt1 n_gt1; rewrite /fpoly_intro_range. by apply: poly_intro_range_auxP. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound