proposition: Lemma eqp_div_XsubC p c : (p == (p %/ ('X - c%:P)) * ('X - c%:P)) = ('X - c%:P %| p).
proof: Proof. by rewrite dvdp_eq lead_coefXsubC expr1n scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)