proposition: Lemma mulp_gcdl p q r : (gcdp p q) * r %= gcdp (p * r) (q * r).
proof: Proof. by rewrite eqp_sym gcdp_mul2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)