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