proposition: Lemma dvdp_eq p : (d %| p) = (p == p %/ d * d).
proof: Proof. apply/eqP/eqP=> [modp0 | ->]; last exact: modp_mull. by rewrite [p in LHS]divp_eq modp0 addr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)