proposition: Lemma divp_mulA p q : d %| q -> p * (q %/ d) = p * q %/ d.
proof: Proof. move=> hdm; apply/eqP; rewrite eq_sym -dvdp_eq_mul. by rewrite -mulrA divpK. by move/divpK: hdm<-; rewrite mulrA dvdp_mull // dvdpp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)