proposition: Lemma coprimep_XsubC p c : coprimep p ('X - c%:P) = ~~ root p c.
proof: Proof. rewrite -coprimep_modl modp_XsubC /root -alg_polyC. have [-> | /coprimepZl->] := eqVneq; last exact: coprime1p. by rewrite scale0r /coprimep gcd0p size_XsubC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)