Add libmGen, a simple generator for mathematical functions

[HeikoBecker]

This PR implements libmGen, a proof-producing translator for elementary functions.
Using the Dandelion and FloVer tools, libmGen automatically validates a polynomial approximation of an elementary function, implements it in CakeML floating-point code, and proves a bound on the approximation error and the roundoff error of the implementation.
The proof is given as a CF specification that relates the floating-point code to the real-numbered elementary function.