proposition: Lemma dvdp_eq p : (q %| p) = (p == (p %/ q) * q).
proof: Proof. by rewrite dvdp_eq (eqP monq) expr1n scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)