proposition: Lemma mu_deriv_root : forall x (p : {poly R}), p != 0 -> root p x -> \mu_x p = (\mu_x (p^`()) + 1)%N.
proof: Proof. by move=> x p p0 rpx; rewrite mu_deriv // subn1 addn1 prednK // mu_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)