proposition: Lemma multiplicity_XsubC p a : {m | exists2 q, (p != 0) ==> ~~ root q a & p = q * ('X - a%:P) ^+ m}.
proof: Proof. have [n le_p_n] := ubnP (size p); elim: n => // n IHn in p le_p_n *. have [-> | nz_p /=] := eqVneq p 0; first by exists 0, 0; rewrite ?mul0r. have [/sig_eqW[p1 Dp] | nz_pa] := altP (factor_theorem p a); last first. by exists 0%N, p; rewrite ?mulr1. have nz_p1: p1 != 0 by apply: contraNneq nz_p => p1_0; rewrite Dp p1_0 mul0r. have /IHn[m /sig2_eqW[q nz_qa Dp1]]: size p1 < n. by rewrite Dp size_Mmonic ?monicXsubC // size_XsubC addn2 in le_p_n. by exists m.+1, q; [rewrite nz_p1 in nz_qa | rewrite exprSr mulrA -Dp1]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)