proposition: Lemma eqp_mulr q p r : p %= q -> p * r %= q * r.
proof: Proof. by move=> epq; rewrite ![_ * r]mulrC eqp_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)