proposition: Lemma rmodn_trans {R : ringType} (p q h z : {poly R}) : h \is monic -> z \is monic -> rdvdp h z -> rmodp p z = rmodp q z -> rmodp p h = rmodp q h.
proof: Proof. move=> hM zM /(rdvdp_trans hM zM) => /(_ (p - q)). rewrite /rdvdp !rmodpB // !subr_eq0 => H /eqP H1; apply/eqP. by apply: H. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound