Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	27475	log plain
-rw-r--r--	AltSeries.v	15634	log plain
-rw-r--r--	ArithProp.v	6978	log plain
-rw-r--r--	Binomial.v	7611	log plain
-rw-r--r--	Cauchy_prod.v	15543	log plain
-rw-r--r--	Cos_plus.v	25951	log plain
-rw-r--r--	Cos_rel.v	11351	log plain
-rw-r--r--	DiscrR.v	2382	log plain
-rw-r--r--	Exp_prop.v	30257	log plain
-rw-r--r--	Integration.v	609	log plain
-rw-r--r--	MVT.v	25466	log plain
-rw-r--r--	Machin.v	6026	log plain
-rw-r--r--	NewtonInt.v	28862	log plain
-rw-r--r--	PSeries_reg.v	9234	log plain
-rw-r--r--	PartSum.v	20056	log plain
-rw-r--r--	RIneq.v	57062	log plain
-rw-r--r--	RList.v	26777	log plain
-rw-r--r--	ROrderedType.v	2737	log plain
-rw-r--r--	R_Ifp.v	39465	log plain
-rw-r--r--	R_sqr.v	11987	log plain
-rw-r--r--	R_sqrt.v	15987	log plain
-rw-r--r--	Ranalysis.v	1056	log plain
-rw-r--r--	Ranalysis1.v	51355	log plain
-rw-r--r--	Ranalysis2.v	16485	log plain
-rw-r--r--	Ranalysis3.v	29825	log plain
-rw-r--r--	Ranalysis4.v	12653	log plain
-rw-r--r--	Ranalysis5.v	57397	log plain
-rw-r--r--	Ranalysis_reg.v	29646	log plain
-rw-r--r--	Ratan.v	61360	log plain
-rw-r--r--	Raxioms.v	5085	log plain
-rw-r--r--	Rbase.v	624	log plain
-rw-r--r--	Rbasic_fun.v	20898	log plain
-rw-r--r--	Rcomplete.v	6731	log plain
-rw-r--r--	Rdefinitions.v	2126	log plain
-rw-r--r--	Rderiv.v	21670	log plain
-rw-r--r--	Reals.v	1400	log plain
-rw-r--r--	Rfunctions.v	24007	log plain
-rw-r--r--	Rgeom.v	7745	log plain
-rw-r--r--	RiemannInt.v	136805	log plain
-rw-r--r--	RiemannInt_SF.v	109986	log plain
-rw-r--r--	Rlimit.v	20809	log plain
-rw-r--r--	Rlogic.v	8332	log plain
-rw-r--r--	Rminmax.v	3645	log plain
-rw-r--r--	Rpow_def.v	657	log plain
-rw-r--r--	Rpower.v	23842	log plain
-rw-r--r--	Rprod.v	6514	log plain
-rw-r--r--	Rseries.v	12478	log plain
-rw-r--r--	Rsigma.v	4918	log plain
-rw-r--r--	Rsqrt_def.v	21578	log plain
-rw-r--r--	Rtopology.v	74279	log plain
-rw-r--r--	Rtrigo.v	993	log plain
-rw-r--r--	Rtrigo1.v	71187	log plain
-rw-r--r--	Rtrigo_alt.v	16862	log plain
-rw-r--r--	Rtrigo_calc.v	15546	log plain
-rw-r--r--	Rtrigo_def.v	14662	log plain
-rw-r--r--	Rtrigo_fun.v	5217	log plain
-rw-r--r--	Rtrigo_reg.v	16895	log plain
-rw-r--r--	SeqProp.v	37719	log plain
-rw-r--r--	SeqSeries.v	15735	log plain
-rw-r--r--	SplitAbsolu.v	892	log plain
-rw-r--r--	SplitRmult.v	776	log plain
-rw-r--r--	Sqrt_reg.v	12734	log plain
-rw-r--r--	intro.tex	122	log plain
-rw-r--r--	vo.itarget	754	log plain