Homotopy Type Theory Sandbox (Rev #31, changes)

Given a real quadratic function $f:\mathbb{R} \to \mathbb{R}$, $f(x) \coloneqq a x^2 + b x + c$ for real numbers $a:\mathbb{R}$, $b:\mathbb{R}$, $c:\mathbb{R}$, where $\vert a \vert \gt 0$, suppose we want to find an approximate zero of $f$. The real quadratic function has discriminant $\Delta = b^2 - 4 a c$ and has 2 zeroes if $\Delta \gt 0$, 1 zero of multiplicity 2 at $2 a x_i + b = 0$ if $\Delta = 0$, or no zeroes of $\Delta \lt 0$. (In constructive mathematics, there are real quadratic functions where it isn’t possible to determine the number of zeroes the real quadratic function has.) Assume that $\Delta \gt 0$. Select a real number $x_0:\mathbb{R}$ as the initial guess, where $2 a x_0 + b \gt 0$ or $2 a x_0 + b \lt 0$, and the next guess would be defined as