proposition: Lemma dvdpZr c m n : c != 0 -> m %| c *: n = (m %| n).
proof: Proof. by move=> cn0; exact/eqp_dvdr/eqp_scale. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)