proposition: Lemma rmodp_Xn_sub1 (R : comRingType) k n : 0 < k -> rmodp ('X^(k * n) - 1) ('X^k - 1) = 0 :> {poly R}.
proof: Proof. move=> k_gt0; elim: n => [|n IH]; first by rewrite muln0 subrr rmod0p. rewrite mulnS exprD -{1}['X^k](subrK 1) mulrDl mul1r. rewrite -addrA rmodpD ?monic_Xn_sub_1 // IH addr0. by rewrite mulrC rmodp_mull ?monic_Xn_sub_1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound