proposition: Lemma is_ipoly1 (R : ringType) k s : is_ipoly k s (1 : {poly R}).
proof: Proof. by move=> m _; apply: introspective1r. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound