proposition: Lemma poly_div_factor (a : R) (P : {poly R} -> Prop) : (forall k, P k%:P) -> (forall p n k, p.[a] != 0 -> P p -> P (p * ('X - a%:P)^+(n.+1) + k%:P)%R) -> forall p, P p.
proof: Proof. move=> Pk Pq p. move: {-2}p (leqnn (size p)); elim: (size p)=> {p} [|n ihn] p spn. by move: spn; rewrite leqn0 size_poly_eq0 -polyC0; move/eqP->; exact: Pk. case: (leqP (size p) 1)=> sp1; first by rewrite [p]size1_polyC ?sp1//. rewrite (Pdiv.IdomainMonic.divp_eq (monicXsubC a) p). rewrite [_ %% _]size1_polyC; last first. by rewrite -ltnS (@leq_trans (size ('X - a%:P))) // ?ltn_modp ?polyXsubC_eq0 ?size_XsubC. have [n' [q hqa hp]] := multiplicity_XsubC (p %/ ('X - a%:P)) a. rewrite divpN0 ?size_XsubC ?polyXsubC_eq0 ?sp1 //= in hqa. rewrite hp -mulrA -exprSr; apply: Pq=> //; apply: ihn. rewrite (@leq_trans (size (q * ('X - a%:P) ^+ n'))) //. rewrite size_mul ?expf_eq0 ?polyXsubC_eq0 ?andbF //; last first. by apply: contraNneq hqa => ->; rewrite root0. by rewrite size_exp_XsubC addnS leq_addr. by rewrite -hp size_divp ?polyXsubC_eq0 ?size_XsubC // leq_subLR. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)