Prove the bound on e^t from Harrison's paper in HOL4
The harrison_1997_material
folder should contain a proof for a bound of e(x)
for x in (0,0.5)
. We need to port this proof to HOL4 to use the McLaurin series lemmas from the base library.
Edited by Heiko Becker