proposition: Lemma dvdp_mul_XsubC p q c : (p %| ('X - c%:P) * q) = ((if root p c then p %/ ('X - c%:P) else p) %| q).
proof: Proof. case: ifPn => [| not_pc0]; last by rewrite Gauss_dvdpr ?coprimep_XsubC. rewrite root_factor_theorem -eqp_div_XsubC mulrC => /eqP{1}->. by rewrite dvdp_mul2l ?polyXsubC_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)