  In complex analysis, the winding number measures the number of times a path
(counter-clockwise) winds around a point, while the Cauchy index can
approximate how the path winds. We formalise this approximation in the Isabelle
theorem prover, and provide a tactic to evaluate winding numbers through Cauchy
indices. By further combining this approximation with the argument principle,
we are able to make use of remainder sequences to effectively count the number
of complex roots of a polynomial within some domains, such as a rectangular box
and a half-plane.
