summaryrefslogtreecommitdiff
path: root/theories7/Reals
ModeNameSize
-rw-r--r--Alembert.v25974logplain
-rw-r--r--AltSeries.v15715logplain
-rw-r--r--ArithProp.v6372logplain
-rw-r--r--Binomial.v7368logplain
-rw-r--r--Cauchy_prod.v14162logplain
-rw-r--r--Cos_plus.v32956logplain
-rw-r--r--Cos_rel.v14079logplain
-rw-r--r--DiscrR.v2784logplain
-rw-r--r--Exp_prop.v30243logplain
-rw-r--r--Integration.v682logplain
-rw-r--r--MVT.v23246logplain
-rw-r--r--NewtonInt.v27097logplain
-rw-r--r--PSeries_reg.v8653logplain
-rw-r--r--PartSum.v18408logplain
-rw-r--r--RIneq.v45888logplain
-rw-r--r--RList.v22699logplain
-rw-r--r--R_Ifp.v27097logplain
-rw-r--r--R_sqr.v10916logplain
-rw-r--r--R_sqrt.v13209logplain
-rw-r--r--Ranalysis.v23767logplain
-rw-r--r--Ranalysis1.v46440logplain
-rw-r--r--Ranalysis2.v16094logplain
-rw-r--r--Ranalysis3.v27830logplain
-rw-r--r--Ranalysis4.v11794logplain
-rw-r--r--Raxioms.v5787logplain
-rw-r--r--Rbase.v691logplain
-rw-r--r--Rbasic_fun.v17557logplain
-rw-r--r--Rcomplete.v6513logplain
-rw-r--r--Rdefinitions.v2197logplain
-rw-r--r--Rderiv.v20837logplain
-rw-r--r--Reals.v1468logplain
-rw-r--r--Rfunctions.v25169logplain
-rw-r--r--Rgeom.v6612logplain
-rw-r--r--RiemannInt.v125014logplain
-rw-r--r--RiemannInt_SF.v99802logplain
-rw-r--r--Rlimit.v21287logplain
-rw-r--r--Rpower.v22460logplain
-rw-r--r--Rprod.v6800logplain
-rw-r--r--Rseries.v9854logplain
-rw-r--r--Rsigma.v5233logplain
-rw-r--r--Rsqrt_def.v19790logplain
-rw-r--r--Rsyntax.v8670logplain
-rw-r--r--Rtopology.v67466logplain
-rw-r--r--Rtrigo.v57532logplain
-rw-r--r--Rtrigo_alt.v18329logplain
-rw-r--r--Rtrigo_calc.v13884logplain
-rw-r--r--Rtrigo_def.v14887logplain
-rw-r--r--Rtrigo_fun.v5542logplain
-rw-r--r--Rtrigo_reg.v21505logplain
-rw-r--r--SeqProp.v39610logplain
-rw-r--r--SeqSeries.v14551logplain
-rw-r--r--SplitAbsolu.v986logplain
-rw-r--r--SplitRmult.v834logplain
-rw-r--r--Sqrt_reg.v12075logplain