proposition: Lemma dvdp_mul2r r p q : r != 0 -> (p * r %| q * r) = (p %| q).
proof: Proof. move=> nzr. have [-> | pn0] := eqVneq p 0. by rewrite mul0r !dvd0p mulf_eq0 (negPf nzr) orbF. have [-> | qn0] := eqVneq q 0; first by rewrite mul0r !dvdp0. apply/idP/idP; last by move=> ?; rewrite dvdp_mul ?dvdpp. rewrite dvdp_eq; set c := _ ^+ _; set x := _ %/ _; move/eqP=> Hx. apply: (@eq_dvdp c x); first by rewrite expf_neq0 // lead_coef_eq0 mulf_neq0. by apply: (mulIf nzr); rewrite -mulrA -scalerAl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)