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