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