proposition: Lemma eqp_coprimepr p q r : q %= r -> coprimep p q = coprimep p r.
proof: Proof. by rewrite -!gcdp_eqp1; move/(eqp_gcdr p)/eqp_ltrans. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)