feat(data/polynomial/root_isolation): root_parity_in_range_of_evals

[BoltonBailey]

A PR to prove that the parity of the number of roots of a real polynomial in a range depends on the signs of the evaluations of the polynomial on either side of the range. Perhaps useful for Descartes rule of signs.

---

• [x] depends on: #14917
• [x] depends on: #14938

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#14917~~
• ~~leanprover-community/mathlib#14938~~ By Dependent Issues (🤖). Happy coding!