Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	.cvsignore	5	log plain
-rw-r--r--	Alembert.v	27332	log plain
-rw-r--r--	AltSeries.v	15785	log plain
-rw-r--r--	ArithProp.v	6800	log plain
-rw-r--r--	Binomial.v	7523	log plain
-rw-r--r--	Cauchy_prod.v	14773	log plain
-rw-r--r--	Cos_plus.v	31828	log plain
-rw-r--r--	Cos_rel.v	12951	log plain
-rw-r--r--	DiscrR.v	2982	log plain
-rw-r--r--	Exp_prop.v	31361	log plain
-rw-r--r--	Integration.v	616	log plain
-rw-r--r--	MVT.v	24498	log plain
-rw-r--r--	NewtonInt.v	28066	log plain
-rw-r--r--	PSeries_reg.v	9250	log plain
-rw-r--r--	PartSum.v	19638	log plain
-rw-r--r--	RIneq.v	47444	log plain
-rw-r--r--	RList.v	26072	log plain
-rw-r--r--	R_Ifp.v	25307	log plain
-rw-r--r--	R_sqr.v	11241	log plain
-rw-r--r--	R_sqrt.v	14315	log plain
-rw-r--r--	Ranalysis.v	28505	log plain
-rw-r--r--	Ranalysis1.v	49736	log plain
-rw-r--r--	Ranalysis2.v	16244	log plain
-rw-r--r--	Ranalysis3.v	28716	log plain
-rw-r--r--	Ranalysis4.v	12425	log plain
-rw-r--r--	Raxioms.v	5133	log plain
-rw-r--r--	Rbase.v	630	log plain
-rw-r--r--	Rbasic_fun.v	17055	log plain
-rw-r--r--	Rcomplete.v	6585	log plain
-rw-r--r--	Rdefinitions.v	2156	log plain
-rw-r--r--	Rderiv.v	18419	log plain
-rw-r--r--	Reals.v	1407	log plain
-rw-r--r--	Rfunctions.v	24555	log plain
-rw-r--r--	Rgeom.v	7503	log plain
-rw-r--r--	RiemannInt.v	132285	log plain
-rw-r--r--	RiemannInt_SF.v	108268	log plain
-rw-r--r--	Rlimit.v	19870	log plain
-rw-r--r--	Rpower.v	22686	log plain
-rw-r--r--	Rprod.v	7139	log plain
-rw-r--r--	Rseries.v	9305	log plain
-rw-r--r--	Rsigma.v	5312	log plain
-rw-r--r--	Rsqrt_def.v	21202	log plain
-rw-r--r--	Rsyntax.v	608	log plain
-rw-r--r--	Rtopology.v	73374	log plain
-rw-r--r--	Rtrigo.v	61307	log plain
-rw-r--r--	Rtrigo_alt.v	17882	log plain
-rw-r--r--	Rtrigo_calc.v	15192	log plain
-rw-r--r--	Rtrigo_def.v	14517	log plain
-rw-r--r--	Rtrigo_fun.v	5144	log plain
-rw-r--r--	Rtrigo_reg.v	22149	log plain
-rw-r--r--	SeqProp.v	41705	log plain
-rw-r--r--	SeqSeries.v	15431	log plain
-rw-r--r--	SplitAbsolu.v	911	log plain
-rw-r--r--	SplitRmult.v	781	log plain
-rw-r--r--	Sqrt_reg.v	12741	log plain
-rw-r--r--	intro.tex	122	log plain