proposition: Lemma dvdp_mul2l r p q: r != 0 -> (r * p %| r * q) = (p %| q).
proof: Proof. by rewrite ![r * _]mulrC; apply: dvdp_mul2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)