proposition: Lemma eqp_coprimepl p q r : q %= r -> coprimep q p = coprimep r p.
proof: Proof. by rewrite !(coprimep_sym _ p); apply: eqp_coprimepr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)