proposition: Lemma eqp_rmodp_dvd (R : ringType) (p1 q r : {poly R}) : p1 \is monic -> (rmodp q p1 == rmodp r p1) = (rdvdp p1 (q - r)).
proof: Proof. by move=> pM; rewrite -subr_eq0 -rmodpB. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound