Numerical Analysis in Rocq