Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	.cvsignore	5	log plain
-rw-r--r--	Alembert.v	27335	log plain
-rw-r--r--	AltSeries.v	15791	log plain
-rw-r--r--	ArithProp.v	6800	log plain
-rw-r--r--	Binomial.v	7527	log plain
-rw-r--r--	Cauchy_prod.v	14778	log plain
-rw-r--r--	Cos_plus.v	31828	log plain
-rw-r--r--	Cos_rel.v	12957	log plain
-rw-r--r--	DiscrR.v	2989	log plain
-rw-r--r--	Exp_prop.v	31366	log plain
-rw-r--r--	Integration.v	623	log plain
-rw-r--r--	MVT.v	24496	log plain
-rw-r--r--	NewtonInt.v	28069	log plain
-rw-r--r--	PSeries_reg.v	9255	log plain
-rw-r--r--	PartSum.v	19631	log plain
-rw-r--r--	RIneq.v	47445	log plain
-rw-r--r--	RList.v	26066	log plain
-rw-r--r--	R_Ifp.v	25313	log plain
-rw-r--r--	R_sqr.v	11248	log plain
-rw-r--r--	R_sqrt.v	14323	log plain
-rw-r--r--	Ranalysis.v	28512	log plain
-rw-r--r--	Ranalysis1.v	49742	log plain
-rw-r--r--	Ranalysis2.v	16250	log plain
-rw-r--r--	Ranalysis3.v	28723	log plain
-rw-r--r--	Ranalysis4.v	12432	log plain
-rw-r--r--	Raxioms.v	5147	log plain
-rw-r--r--	Rbase.v	637	log plain
-rw-r--r--	Rbasic_fun.v	17062	log plain
-rw-r--r--	Rcomplete.v	6589	log plain
-rw-r--r--	Rdefinitions.v	2163	log plain
-rw-r--r--	Rderiv.v	18426	log plain
-rw-r--r--	Reals.v	1414	log plain
-rw-r--r--	Rfunctions.v	24781	log plain
-rw-r--r--	Rgeom.v	7510	log plain
-rw-r--r--	RiemannInt.v	132218	log plain
-rw-r--r--	RiemannInt_SF.v	108254	log plain
-rw-r--r--	Rlimit.v	19878	log plain
-rw-r--r--	Rpower.v	22697	log plain
-rw-r--r--	Rprod.v	7153	log plain
-rw-r--r--	Rseries.v	9313	log plain
-rw-r--r--	Rsigma.v	5319	log plain
-rw-r--r--	Rsqrt_def.v	21212	log plain
-rw-r--r--	Rtopology.v	73238	log plain
-rw-r--r--	Rtrigo.v	61307	log plain
-rw-r--r--	Rtrigo_alt.v	17888	log plain
-rw-r--r--	Rtrigo_calc.v	15199	log plain
-rw-r--r--	Rtrigo_def.v	14524	log plain
-rw-r--r--	Rtrigo_fun.v	5151	log plain
-rw-r--r--	Rtrigo_reg.v	22151	log plain
-rw-r--r--	SeqProp.v	41690	log plain
-rw-r--r--	SeqSeries.v	15436	log plain
-rw-r--r--	SplitAbsolu.v	918	log plain
-rw-r--r--	SplitRmult.v	788	log plain
-rw-r--r--	Sqrt_reg.v	12744	log plain
-rw-r--r--	intro.tex	122	log plain