proposition: Lemma is_ipoly_Xaddc (R : ringType) k s c : 0 <= c <= s -> is_ipoly k s ('X + c%:R%:P : {poly R}).
proof: Proof. rewrite leq_eqVlt; case: eqP => /= [<- _ m _|_ cB m [_]]; last by apply. by rewrite addr0; apply: introspectiveX. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound