Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	.cvsignore	5	log plain
-rw-r--r--	Alembert.v	25911	log plain
-rw-r--r--	AltSeries.v	15651	log plain
-rw-r--r--	ArithProp.v	6308	log plain
-rw-r--r--	Binomial.v	7305	log plain
-rw-r--r--	Cauchy_prod.v	14096	log plain
-rw-r--r--	Cos_plus.v	32893	log plain
-rw-r--r--	Cos_rel.v	14017	log plain
-rw-r--r--	DiscrR.v	2723	log plain
-rw-r--r--	Exp_prop.v	30180	log plain
-rw-r--r--	Integration.v	616	log plain
-rw-r--r--	MVT.v	23188	log plain
-rw-r--r--	NewtonInt.v	27033	log plain
-rw-r--r--	PSeries_reg.v	8587	log plain
-rw-r--r--	PartSum.v	18346	log plain
-rw-r--r--	RIneq.v	45074	log plain
-rw-r--r--	RList.v	22639	log plain
-rw-r--r--	R_Ifp.v	27037	log plain
-rw-r--r--	R_sqr.v	10856	log plain
-rw-r--r--	R_sqrt.v	13148	log plain
-rw-r--r--	Ranalysis.v	23703	log plain
-rw-r--r--	Ranalysis1.v	46375	log plain
-rw-r--r--	Ranalysis2.v	16029	log plain
-rw-r--r--	Ranalysis3.v	27765	log plain
-rw-r--r--	Ranalysis4.v	11729	log plain
-rw-r--r--	Raxioms.v	5723	log plain
-rw-r--r--	Rbase.v	631	log plain
-rw-r--r--	Rbasic_fun.v	17491	log plain
-rw-r--r--	Rcomplete.v	6449	log plain
-rw-r--r--	Rdefinitions.v	2156	log plain
-rw-r--r--	Rderiv.v	20776	log plain
-rw-r--r--	Reals.v	1408	log plain
-rw-r--r--	Rfunctions.v	25142	log plain
-rw-r--r--	Rgeom.v	6552	log plain
-rw-r--r--	RiemannInt.v	124949	log plain
-rw-r--r--	RiemannInt_SF.v	99738	log plain
-rw-r--r--	Rlimit.v	21226	log plain
-rw-r--r--	Rpower.v	22330	log plain
-rw-r--r--	Rprod.v	6740	log plain
-rw-r--r--	Rseries.v	9792	log plain
-rw-r--r--	Rsigma.v	5172	log plain
-rw-r--r--	Rsqrt_def.v	19726	log plain
-rw-r--r--	Rsyntax.v	8608	log plain
-rw-r--r--	Rtopology.v	67402	log plain
-rw-r--r--	Rtrigo.v	57471	log plain
-rw-r--r--	Rtrigo_alt.v	18264	log plain
-rw-r--r--	Rtrigo_calc.v	13818	log plain
-rw-r--r--	Rtrigo_def.v	14822	log plain
-rw-r--r--	Rtrigo_fun.v	5477	log plain
-rw-r--r--	Rtrigo_reg.v	21440	log plain
-rw-r--r--	SeqProp.v	40044	log plain
-rw-r--r--	SeqSeries.v	14487	log plain
-rw-r--r--	SplitAbsolu.v	920	log plain
-rw-r--r--	SplitRmult.v	769	log plain
-rw-r--r--	Sqrt_reg.v	12012	log plain
-rw-r--r--	intro.tex	122	log plain