aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Ranalysis5.v
AgeCommit message (Expand)Author
2012-06-11finish the rearrangement for removing the sin_PI2 axiom. This new versionbertot
2012-06-11Adds the proof of PI_ineq, plus some other smarter ways to approximate PIbertot