proposition: Lemma eqp_mull r p q: q %= r -> p * q %= p * r.
proof: Proof. case/eqpP=> [[c d]] /andP [c0 d0 e]; apply/eqpP; exists (c, d); rewrite ?c0 //. by rewrite scalerAr e -scalerAr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)