proposition: Lemma coprimepZl c m n : c != 0 -> coprimep (c *: m) n = coprimep m n.
proof: Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scalel _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)