proposition: Lemma dvdp_XsubCl p x : ('X - x%:P) %| p = root p x.
proof: Proof. by rewrite dvdpE; apply: Ring.rdvdp_XsubCl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)