proposition: Lemma eqp_dvdl d2 d1 p : d1 %= d2 -> d1 %| p = (d2 %| p).
proof: Proof. suff Hmn m n: m %= n -> (m %| p) -> (n %| p). by move=> ?; apply/idP/idP; apply: Hmn; rewrite // eqp_sym. by rewrite /eqp; case/andP=> dd' d'd dp; apply: (dvdp_trans d'd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)