Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	25900	log plain
-rw-r--r--	AltSeries.v	15579	log plain
-rw-r--r--	ArithProp.v	6210	log plain
-rw-r--r--	Binomial.v	7233	log plain
-rw-r--r--	Cauchy_prod.v	14024	log plain
-rw-r--r--	Cos_plus.v	32819	log plain
-rw-r--r--	Cos_rel.v	13945	log plain
-rw-r--r--	DiscrR.v	2687	log plain
-rw-r--r--	Exp_prop.v	30083	log plain
-rw-r--r--	Integration.v	616	log plain
-rw-r--r--	MVT.v	23077	log plain
-rw-r--r--	NewtonInt.v	26969	log plain
-rw-r--r--	PSeries_reg.v	8551	log plain
-rw-r--r--	PartSum.v	18274	log plain
-rw-r--r--	RIneq.v	44694	log plain
-rw-r--r--	RList.v	22567	log plain
-rw-r--r--	R_Ifp.v	26949	log plain
-rw-r--r--	R_sqr.v	10820	log plain
-rw-r--r--	R_sqrt.v	13112	log plain
-rw-r--r--	Ranalysis.v	23667	log plain
-rw-r--r--	Ranalysis1.v	45510	log plain
-rw-r--r--	Ranalysis2.v	15993	log plain
-rw-r--r--	Ranalysis3.v	27729	log plain
-rw-r--r--	Ranalysis4.v	11693	log plain
-rw-r--r--	Raxioms.v	5219	log plain
-rw-r--r--	Rbase.v	658	log plain
-rw-r--r--	Rbasic_fun.v	17424	log plain
-rw-r--r--	Rcomplete.v	6377	log plain
-rw-r--r--	Rdefinitions.v	1466	log plain
-rw-r--r--	Rderiv.v	20740	log plain
-rw-r--r--	Reals.v	1408	log plain
-rw-r--r--	Rfunctions.v	24971	log plain
-rw-r--r--	Rgeom.v	6516	log plain
-rw-r--r--	RiemannInt.v	124745	log plain
-rw-r--r--	RiemannInt_SF.v	99459	log plain
-rw-r--r--	Rlimit.v	21190	log plain
-rw-r--r--	Rpower.v	22294	log plain
-rw-r--r--	Rprod.v	6668	log plain
-rw-r--r--	Rseries.v	9675	log plain
-rw-r--r--	Rsigma.v	5100	log plain
-rw-r--r--	Rsqrt_def.v	19654	log plain
-rw-r--r--	Rsyntax.v	8976	log plain
-rw-r--r--	Rtopology.v	67366	log plain
-rw-r--r--	Rtrigo.v	57373	log plain
-rw-r--r--	Rtrigo_alt.v	18192	log plain
-rw-r--r--	Rtrigo_calc.v	13746	log plain
-rw-r--r--	Rtrigo_def.v	14750	log plain
-rw-r--r--	Rtrigo_fun.v	5389	log plain
-rw-r--r--	Rtrigo_reg.v	21332	log plain
-rw-r--r--	SeqProp.v	40344	log plain
-rw-r--r--	SeqSeries.v	14414	log plain
-rw-r--r--	SplitAbsolu.v	920	log plain
-rw-r--r--	SplitRmult.v	769	log plain
-rw-r--r--	Sqrt_reg.v	11976	log plain
-rw-r--r--	TypeSyntax.v	1223	log plain
-rw-r--r--	intro.tex	122	log plain