Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	28619	log plain
-rw-r--r--	AltSeries.v	16134	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	31593	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--	NewtonInt.v	29501	log plain
-rw-r--r--	PSeries_reg.v	9538	log plain
-rw-r--r--	PartSum.v	20688	log plain
-rw-r--r--	RIneq.v	57213	log plain
-rw-r--r--	RList.v	27793	log plain
-rw-r--r--	ROrderedType.v	2739	log plain
-rw-r--r--	R_Ifp.v	39774	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	29645	log plain
-rw-r--r--	Ranalysis1.v	53504	log plain
-rw-r--r--	Ranalysis2.v	16899	log plain
-rw-r--r--	Ranalysis3.v	30473	log plain
-rw-r--r--	Ranalysis4.v	13124	log plain
-rw-r--r--	Raxioms.v	5105	log plain
-rw-r--r--	Rbase.v	624	log plain
-rw-r--r--	Rbasic_fun.v	21280	log plain
-rw-r--r--	Rcomplete.v	6915	log plain
-rw-r--r--	Rdefinitions.v	2126	log plain
-rw-r--r--	Rderiv.v	22245	log plain
-rw-r--r--	Reals.v	1400	log plain
-rw-r--r--	Rfunctions.v	24118	log plain
-rw-r--r--	Rgeom.v	7856	log plain
-rw-r--r--	RiemannInt.v	140786	log plain
-rw-r--r--	RiemannInt_SF.v	114302	log plain
-rw-r--r--	Rlimit.v	21384	log plain
-rw-r--r--	Rlogic.v	8322	log plain
-rw-r--r--	Rminmax.v	3645	log plain
-rw-r--r--	Rpow_def.v	657	log plain
-rw-r--r--	Rpower.v	24513	log plain
-rw-r--r--	Rprod.v	6586	log plain
-rw-r--r--	Rseries.v	12629	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	66364	log plain
-rw-r--r--	Rtrigo_alt.v	17824	log plain
-rw-r--r--	Rtrigo_calc.v	16073	log plain
-rw-r--r--	Rtrigo_def.v	15086	log plain
-rw-r--r--	Rtrigo_fun.v	5291	log plain
-rw-r--r--	Rtrigo_reg.v	23121	log plain
-rw-r--r--	SeqProp.v	38879	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	709	log plain