Abstract: 
Descartes' Rule of Signs relates the number of positive real roots of a
polynomial with the number of sign changes in its coefficient sequence.
Our proof follows the simple inductive proof given by Rob Arthan, which was also
used by John Harrison in his HOL Light formalisation. We proved most of the
lemmas for arbitrary linearlyordered integrity domains (e.g. integers,
rationals, reals); the main result, however, requires the intermediate value
theorem and was therefore only proven for real polynomials.

BibTeX: 
@article{Descartes_Sign_RuleAFP,
author = {Manuel Eberl},
title = {Descartes' Rule of Signs},
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{http://isaafp.org/entries/Descartes_Sign_Rule.html},
Formal proof development},
ISSN = {2150914x},
}
