  Many problems in computer algebra and numerical analysis can be reduced to
counting or approximating the real roots of a polynomial within an interval.
Existing verified root-counting procedures in major proof assistants are mainly
based on the classical Sturm theorem, which only counts distinct roots.
  In this paper, we have strengthened the root-counting ability in Isabelle/HOL
by first formally proving the Budan-Fourier theorem. Subsequently, based on
Descartes' rule of signs and Taylor shift, we have provided a verified
procedure to efficiently over-approximate the number of real roots within an
interval, counting multiplicity. For counting multiple roots exactly, we have
extended our previous formalisation of Sturm's theorem. Finally, we combine
verified components in the developments above to improve our previous certified
complex-root-counting procedures based on Cauchy indices. We believe those
verified routines will be crucial for certifying programs and building tactics.
