Implicit function theorem

[bmsherman]

When the diff function in Newton.ml tries to compute the derivative with respect to a Dedekind cut that involves the variable being differentiated, it gives up.
If we want to compute the derivative of e with respect to x, and e is of the form

cut q
  left  f(q, x) < g(q, x)
  right g(q, x) < f(q, x) 

then, letting h(q, x) = g(q, x) - f(q, x), we can use the implicit function theorem to say that the derivative of e with respect to x is

- (diff h x) / (diff h q)

, where we use the interval approximation for q in the result there.