Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	29543	log plain
-rw-r--r--	Alembert_compl.v	10474	log plain
-rw-r--r--	AltSeries.v	18763	log plain
-rw-r--r--	Binome.v	9670	log plain
-rw-r--r--	Cauchy_prod.v	14004	log plain
-rw-r--r--	Cos_plus.v	35610	log plain
-rw-r--r--	Cos_rel.v	14705	log plain
-rw-r--r--	Cv_prop.v	9541	log plain
-rw-r--r--	DiscrR.v	1808	log plain
-rw-r--r--	PSeries_reg.v	22025	log plain
-rw-r--r--	R_Ifp.v	26956	log plain
-rw-r--r--	R_sqr.v	10827	log plain
-rw-r--r--	R_sqrt.v	13379	log plain
-rw-r--r--	Ranalysis.v	642	log plain
-rw-r--r--	Ranalysis1.v	56199	log plain
-rw-r--r--	Ranalysis2.v	16225	log plain
-rw-r--r--	Ranalysis3.v	27688	log plain
-rw-r--r--	Ranalysis4.v	36458	log plain
-rw-r--r--	Raxioms.v	5138	log plain
-rw-r--r--	Rbase.v	44539	log plain
-rw-r--r--	Rbasic_fun.v	16266	log plain
-rw-r--r--	Rcomplet.v	23708	log plain
-rw-r--r--	Rdefinitions.v	1440	log plain
-rw-r--r--	Rderiv.v	20691	log plain
-rw-r--r--	Reals.v	1132	log plain
-rw-r--r--	Rfunctions.v	19258	log plain
-rw-r--r--	Rgeom.v	6477	log plain
-rw-r--r--	Rlimit.v	23475	log plain
-rw-r--r--	Rprod.v	6229	log plain
-rw-r--r--	Rseries.v	9668	log plain
-rw-r--r--	Rsigma.v	5324	log plain
-rw-r--r--	Rsqrt_def.v	19813	log plain
-rw-r--r--	Rsyntax.v	6911	log plain
-rw-r--r--	Rtrigo.v	60882	log plain
-rw-r--r--	Rtrigo_alt.v	28747	log plain
-rw-r--r--	Rtrigo_calc.v	14670	log plain
-rw-r--r--	Rtrigo_def.v	16801	log plain
-rw-r--r--	Rtrigo_fun.v	5359	log plain
-rw-r--r--	Rtrigo_reg.v	21446	log plain
-rw-r--r--	SplitAbsolu.v	907	log plain
-rw-r--r--	SplitRmult.v	759	log plain
-rw-r--r--	Sqrt_reg.v	12022	log plain
-rw-r--r--	TypeSyntax.v	1178	log plain
-rw-r--r--	intro.tex	122	log plain