proposition: Lemma mu_spec p a : p != 0 -> { q : {poly R} & (~~ root q a) & ( p = q * ('X - a%:P) ^+ (\mu_a p)) }.
proof: Proof. move=> nz_p; rewrite /multiplicity -if_neg. by case: (_ p a) => m /=/sig2_eqW[q]; rewrite nz_p; exists q. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)