proposition: Lemma coprimep_addl_mul p q r : coprimep r (p * r + q) = coprimep r q.
proof: Proof. by rewrite !coprimep_def (eqp_size (gcdp_addl_mul _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)