proposition: Lemma rdvdp_XsubCl p x : rdvdp ('X - x%:P) p = root p x.
proof: Proof. have [HcX Hr] := monic_comreg (monicXsubC x). apply/rmodp_eq0P/factor_theorem => [|[p1 ->]]; last exact/rmodp_mull/monicXsubC. move=> e0; exists (rdivp p ('X - x%:P)). by rewrite [LHS](rdivp_eq (monicXsubC x)) e0 addr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)