aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Ranalysis5.v
AgeCommit message (Expand)Author
2013-12-03Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Guillaume Melquiond
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
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