Reals « theories7 - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	.cvsignore	5	log plain
-rw-r--r--	Alembert.v	25918	log plain
-rw-r--r--	AltSeries.v	15658	log plain
-rw-r--r--	ArithProp.v	6315	log plain
-rw-r--r--	Binomial.v	7312	log plain
-rw-r--r--	Cauchy_prod.v	14103	log plain
-rw-r--r--	Cos_plus.v	32900	log plain
-rw-r--r--	Cos_rel.v	14024	log plain
-rw-r--r--	DiscrR.v	2730	log plain
-rw-r--r--	Exp_prop.v	30187	log plain
-rw-r--r--	Integration.v	623	log plain
-rw-r--r--	MVT.v	23195	log plain
-rw-r--r--	NewtonInt.v	27040	log plain
-rw-r--r--	PSeries_reg.v	8594	log plain
-rw-r--r--	PartSum.v	18353	log plain
-rw-r--r--	RIneq.v	45835	log plain
-rw-r--r--	RList.v	22646	log plain
-rw-r--r--	R_Ifp.v	27044	log plain
-rw-r--r--	R_sqr.v	10863	log plain
-rw-r--r--	R_sqrt.v	13155	log plain
-rw-r--r--	Ranalysis.v	23710	log plain
-rw-r--r--	Ranalysis1.v	46382	log plain
-rw-r--r--	Ranalysis2.v	16036	log plain
-rw-r--r--	Ranalysis3.v	27772	log plain
-rw-r--r--	Ranalysis4.v	11736	log plain
-rw-r--r--	Raxioms.v	5732	log plain
-rw-r--r--	Rbase.v	638	log plain
-rw-r--r--	Rbasic_fun.v	17499	log plain
-rw-r--r--	Rcomplete.v	6456	log plain
-rw-r--r--	Rdefinitions.v	2137	log plain
-rw-r--r--	Rderiv.v	20783	log plain
-rw-r--r--	Reals.v	1415	log plain
-rw-r--r--	Rfunctions.v	25111	log plain
-rw-r--r--	Rgeom.v	6559	log plain
-rw-r--r--	RiemannInt.v	124956	log plain
-rw-r--r--	RiemannInt_SF.v	99741	log plain
-rw-r--r--	Rlimit.v	21233	log plain
-rw-r--r--	Rpower.v	22406	log plain
-rw-r--r--	Rprod.v	6747	log plain
-rw-r--r--	Rseries.v	9799	log plain
-rw-r--r--	Rsigma.v	5179	log plain
-rw-r--r--	Rsqrt_def.v	19733	log plain
-rw-r--r--	Rsyntax.v	8615	log plain
-rw-r--r--	Rtopology.v	67409	log plain
-rw-r--r--	Rtrigo.v	57478	log plain
-rw-r--r--	Rtrigo_alt.v	18271	log plain
-rw-r--r--	Rtrigo_calc.v	13825	log plain
-rw-r--r--	Rtrigo_def.v	14829	log plain
-rw-r--r--	Rtrigo_fun.v	5484	log plain
-rw-r--r--	Rtrigo_reg.v	21447	log plain
-rw-r--r--	SeqProp.v	39555	log plain
-rw-r--r--	SeqSeries.v	14494	log plain
-rw-r--r--	SplitAbsolu.v	927	log plain
-rw-r--r--	SplitRmult.v	776	log plain
-rw-r--r--	Sqrt_reg.v	12019	log plain