proposition: Lemma coprimep_map p q : coprimep p^f q^f = coprimep p q.
proof: Proof. by rewrite -!gcdp_eqp1 -eqp_map rmorph1 gcdp_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)