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