Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	28619	log plain
-rw-r--r--	AltSeries.v	16162	log plain
-rw-r--r--	ArithProp.v	7186	log plain
-rw-r--r--	Binomial.v	7907	log plain
-rw-r--r--	Cauchy_prod.v	15647	log plain
-rw-r--r--	Cos_plus.v	26759	log plain
-rw-r--r--	Cos_rel.v	11743	log plain
-rw-r--r--	DiscrR.v	2406	log plain
-rw-r--r--	Exp_prop.v	31146	log plain
-rw-r--r--	Integration.v	609	log plain
-rw-r--r--	LegacyRfield.v	1225	log plain
-rw-r--r--	MVT.v	25866	log plain
-rw-r--r--	Machin.v	6026	log plain
-rw-r--r--	NewtonInt.v	29502	log plain
-rw-r--r--	PSeries_reg.v	9538	log plain
-rw-r--r--	PartSum.v	20688	log plain
-rw-r--r--	RIneq.v	57793	log plain
-rw-r--r--	RList.v	27793	log plain
-rw-r--r--	ROrderedType.v	2737	log plain
-rw-r--r--	R_Ifp.v	39769	log plain
-rw-r--r--	R_sqr.v	12115	log plain
-rw-r--r--	R_sqrt.v	16195	log plain
-rw-r--r--	Ranalysis.v	1056	log plain
-rw-r--r--	Ranalysis1.v	53163	log plain
-rw-r--r--	Ranalysis2.v	16901	log plain
-rw-r--r--	Ranalysis3.v	30473	log plain
-rw-r--r--	Ranalysis4.v	13125	log plain
-rw-r--r--	Ranalysis5.v	57397	log plain
-rw-r--r--	Ranalysis_reg.v	29646	log plain
-rw-r--r--	Ratan.v	61353	log plain
-rw-r--r--	Raxioms.v	5085	log plain
-rw-r--r--	Rbase.v	624	log plain
-rw-r--r--	Rbasic_fun.v	21282	log plain
-rw-r--r--	Rcomplete.v	6915	log plain
-rw-r--r--	Rdefinitions.v	2126	log plain
-rw-r--r--	Rderiv.v	22230	log plain
-rw-r--r--	Reals.v	1400	log plain
-rw-r--r--	Rfunctions.v	24089	log plain
-rw-r--r--	Rgeom.v	7857	log plain
-rw-r--r--	RiemannInt.v	140790	log plain
-rw-r--r--	RiemannInt_SF.v	114306	log plain
-rw-r--r--	Rlimit.v	21377	log plain
-rw-r--r--	Rlogic.v	8364	log plain
-rw-r--r--	Rminmax.v	3645	log plain
-rw-r--r--	Rpow_def.v	657	log plain
-rw-r--r--	Rpower.v	24514	log plain
-rw-r--r--	Rprod.v	6586	log plain
-rw-r--r--	Rseries.v	12614	log plain
-rw-r--r--	Rsigma.v	5054	log plain
-rw-r--r--	Rsqrt_def.v	22434	log plain
-rw-r--r--	Rtopology.v	77943	log plain
-rw-r--r--	Rtrigo.v	993	log plain
-rw-r--r--	Rtrigo1.v	75951	log plain
-rw-r--r--	Rtrigo_alt.v	17486	log plain
-rw-r--r--	Rtrigo_calc.v	16074	log plain
-rw-r--r--	Rtrigo_def.v	15086	log plain
-rw-r--r--	Rtrigo_fun.v	5281	log plain
-rw-r--r--	Rtrigo_reg.v	17583	log plain
-rw-r--r--	SeqProp.v	38863	log plain
-rw-r--r--	SeqSeries.v	16159	log plain
-rw-r--r--	SplitAbsolu.v	900	log plain
-rw-r--r--	SplitRmult.v	776	log plain
-rw-r--r--	Sqrt_reg.v	13438	log plain
-rw-r--r--	intro.tex	122	log plain
-rw-r--r--	vo.itarget	770	log plain