If I was courageous enough, I would finish packaging these proofs and make sure they are distributed in the user's contributions of the Coq system, but some of them really are only small examples.
Proving the convergence of a sequence based on algebraic-geometric means to PI. This example relies on the coquelicot library developed by colleagues in Saclay. It contains examples of improper integrals, properties of uniformly convergent sequences of functions, arcsinh, variable changes in integrals, etc. The latest version is compatible with version 2 of coquelicot. The tar archive also contains files to really compute one million decimals of PI, together with the proof of correctness (tested with coq-8.4pl6 and coquelicot 2.0.1).