Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	27456	log plain
-rw-r--r--	AltSeries.v	15578	log plain
-rw-r--r--	ArithProp.v	6987	log plain
-rw-r--r--	Binomial.v	7516	log plain
-rw-r--r--	Cauchy_prod.v	15543	log plain
-rw-r--r--	Cos_plus.v	25973	log plain
-rw-r--r--	Cos_rel.v	10499	log plain
-rw-r--r--	DiscrR.v	2403	log plain
-rw-r--r--	Exp_prop.v	30283	log plain
-rw-r--r--	Integration.v	609	log plain
-rw-r--r--	MVT.v	26479	log plain
-rw-r--r--	Machin.v	6609	log plain
-rw-r--r--	NewtonInt.v	27593	log plain
-rw-r--r--	PSeries_reg.v	24816	log plain
-rw-r--r--	PartSum.v	19993	log plain
-rw-r--r--	RIneq.v	58621	log plain
-rw-r--r--	RList.v	26767	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	11821	log plain
-rw-r--r--	R_sqrt.v	16111	log plain
-rw-r--r--	Ranalysis.v	1056	log plain
-rw-r--r--	Ranalysis1.v	53845	log plain
-rw-r--r--	Ranalysis2.v	16515	log plain
-rw-r--r--	Ranalysis3.v	29825	log plain
-rw-r--r--	Ranalysis4.v	13095	log plain
-rw-r--r--	Ranalysis5.v	55802	log plain
-rw-r--r--	Ranalysis_reg.v	29673	log plain
-rw-r--r--	Ratan.v	62124	log plain
-rw-r--r--	Raxioms.v	5085	log plain
-rw-r--r--	Rbase.v	624	log plain
-rw-r--r--	Rbasic_fun.v	21500	log plain
-rw-r--r--	Rcomplete.v	6698	log plain
-rw-r--r--	Rdefinitions.v	2126	log plain
-rw-r--r--	Rderiv.v	21703	log plain
-rw-r--r--	Reals.v	1400	log plain
-rw-r--r--	Rfunctions.v	24329	log plain
-rw-r--r--	Rgeom.v	7745	log plain
-rw-r--r--	RiemannInt.v	136009	log plain
-rw-r--r--	RiemannInt_SF.v	108453	log plain
-rw-r--r--	Rlimit.v	20908	log plain
-rw-r--r--	Rlogic.v	5541	log plain
-rw-r--r--	Rminmax.v	3645	log plain
-rw-r--r--	Rpow_def.v	657	log plain
-rw-r--r--	Rpower.v	28717	log plain
-rw-r--r--	Rprod.v	6536	log plain
-rw-r--r--	Rseries.v	13323	log plain
-rw-r--r--	Rsigma.v	4940	log plain
-rw-r--r--	Rsqrt_def.v	21595	log plain
-rw-r--r--	Rtopology.v	73237	log plain
-rw-r--r--	Rtrigo.v	963	log plain
-rw-r--r--	Rtrigo1.v	71181	log plain
-rw-r--r--	Rtrigo_alt.v	16279	log plain
-rw-r--r--	Rtrigo_calc.v	15546	log plain
-rw-r--r--	Rtrigo_def.v	14672	log plain
-rw-r--r--	Rtrigo_fun.v	5388	log plain
-rw-r--r--	Rtrigo_reg.v	16908	log plain
-rw-r--r--	SeqProp.v	37554	log plain
-rw-r--r--	SeqSeries.v	15782	log plain
-rw-r--r--	SplitAbsolu.v	911	log plain
-rw-r--r--	SplitRmult.v	776	log plain
-rw-r--r--	Sqrt_reg.v	12702	log plain
-rw-r--r--	intro.tex	122	log plain
-rw-r--r--	vo.itarget	754	log plain