aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
ModeNameSize
-rw-r--r--Alembert.v27447logplain
-rw-r--r--AltSeries.v14384logplain
-rw-r--r--ArithProp.v6989logplain
-rw-r--r--Binomial.v7516logplain
-rw-r--r--Cauchy_prod.v15543logplain
-rw-r--r--Cos_plus.v25899logplain
-rw-r--r--Cos_rel.v10540logplain
-rw-r--r--DiscrR.v2034logplain
-rw-r--r--Exp_prop.v30106logplain
-rw-r--r--Integration.v609logplain
-rw-r--r--MVT.v26479logplain
-rw-r--r--Machin.v6642logplain
-rw-r--r--NewtonInt.v27593logplain
-rw-r--r--PSeries_reg.v24858logplain
-rw-r--r--PartSum.v19993logplain
-rw-r--r--RIneq.v58142logplain
-rw-r--r--RList.v26767logplain
-rw-r--r--ROrderedType.v2737logplain
-rw-r--r--R_Ifp.v37805logplain
-rw-r--r--R_sqr.v10503logplain
-rw-r--r--R_sqrt.v12374logplain
-rw-r--r--Ranalysis.v1057logplain
-rw-r--r--Ranalysis1.v53845logplain
-rw-r--r--Ranalysis2.v16027logplain
-rw-r--r--Ranalysis3.v29406logplain
-rw-r--r--Ranalysis4.v12863logplain
-rw-r--r--Ranalysis5.v55533logplain
-rw-r--r--Ranalysis_reg.v30125logplain
-rw-r--r--Ratan.v60945logplain
-rw-r--r--Raxioms.v4722logplain
-rw-r--r--Rbase.v624logplain
-rw-r--r--Rbasic_fun.v21319logplain
-rw-r--r--Rcomplete.v6698logplain
-rw-r--r--Rdefinitions.v2802logplain
-rw-r--r--Rderiv.v21457logplain
-rw-r--r--Reals.v1400logplain
-rw-r--r--Rfunctions.v27145logplain
-rw-r--r--Rgeom.v7745logplain
-rw-r--r--RiemannInt.v136009logplain
-rw-r--r--RiemannInt_SF.v108369logplain
-rw-r--r--Rlimit.v20042logplain
-rw-r--r--Rlogic.v5541logplain
-rw-r--r--Rminmax.v3645logplain
-rw-r--r--Rpow_def.v656logplain
-rw-r--r--Rpower.v28320logplain
-rw-r--r--Rprod.v6536logplain
-rw-r--r--Rseries.v13318logplain
-rw-r--r--Rsigma.v4940logplain
-rw-r--r--Rsqrt_def.v21590logplain
-rw-r--r--Rtopology.v73237logplain
-rw-r--r--Rtrigo.v963logplain
-rw-r--r--Rtrigo1.v65247logplain
-rw-r--r--Rtrigo_alt.v15462logplain
-rw-r--r--Rtrigo_calc.v11120logplain
-rw-r--r--Rtrigo_def.v13941logplain
-rw-r--r--Rtrigo_fun.v5388logplain
-rw-r--r--Rtrigo_reg.v16429logplain
-rw-r--r--SeqProp.v37471logplain
-rw-r--r--SeqSeries.v15782logplain
-rw-r--r--SplitAbsolu.v911logplain
-rw-r--r--SplitRmult.v776logplain
-rw-r--r--Sqrt_reg.v12729logplain