Library Coq.Reals.AltSeries
Formalization of alternated series
A more general inequality
This lemma gives an interesting result about alternated series
Convergence of alternated series
Application : construction of PI
Now, PI is defined
We can get an approximation of PI with the following inequality