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