Port upper bound lemmas from John Harrisons material to HOL4

This ports some of the proofs in drang.ml to a file drangScript.sml. The theorems are used by the Harrison paper to establish a relation between the roots found via sturm's theorem and the global upper bound; i.e. they prove that if a polynomial reaches an extrema on the outer points and all places where its derivative is zero, the upper bound is a global upper bound. These should be crucial for justifying soundness of Dandelion later on.