Fully polymorphic numerical method: Bisection

Stream: mathlib4

[Oscar Matemb ⚛️]

I’ve implemented a fully polymorphic bisection method here. It finds a root in the interval [a, b], and when executing on floats, it agrees with Python numerical libraries works quite nicely when executing on floats. We made make it fully polymorphic to work with both Floats and ℝ, and prove termination and sub-interval generation thus far. Beyond these, what other properties, theorems or invariants about the code are there that are typically proved in this context?
I redefined mathlib definitions for now to get the code to agree with reals. Any questions, suggestions and critiques on style, refactoring and so on... are welcomed as well.