Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	26038	log plain
-rw-r--r--	AltSeries.v	15734	log plain
-rw-r--r--	ArithProp.v	6244	log plain
-rw-r--r--	Binome.v	7239	log plain
-rw-r--r--	Cauchy_prod.v	14007	log plain
-rw-r--r--	Cos_plus.v	32766	log plain
-rw-r--r--	Cos_rel.v	13927	log plain
-rw-r--r--	DiscrR.v	1951	log plain
-rw-r--r--	Exp_prop.v	30223	log plain
-rw-r--r--	Integration.v	616	log plain
-rw-r--r--	NewtonInt.v	26983	log plain
-rw-r--r--	PSeries_reg.v	8499	log plain
-rw-r--r--	PartSum.v	18268	log plain
-rw-r--r--	RIneq.v	45036	log plain
-rw-r--r--	RList.v	22815	log plain
-rw-r--r--	R_Ifp.v	26949	log plain
-rw-r--r--	R_sqr.v	10820	log plain
-rw-r--r--	R_sqrt.v	13096	log plain
-rw-r--r--	Ranalysis.v	23698	log plain
-rw-r--r--	Ranalysis1.v	45493	log plain
-rw-r--r--	Ranalysis2.v	16110	log plain
-rw-r--r--	Ranalysis3.v	27804	log plain
-rw-r--r--	Ranalysis4.v	11677	log plain
-rw-r--r--	Raxioms.v	5138	log plain
-rw-r--r--	Rbase.v	658	log plain
-rw-r--r--	Rbasic_fun.v	17408	log plain
-rw-r--r--	Rcomplet.v	6293	log plain
-rw-r--r--	Rdefinitions.v	1440	log plain
-rw-r--r--	Rderiv.v	20724	log plain
-rw-r--r--	Reals.v	685	log plain
-rw-r--r--	Rfunctions.v	24986	log plain
-rw-r--r--	Rgeom.v	6501	log plain
-rw-r--r--	RiemannInt.v	124035	log plain
-rw-r--r--	RiemannInt_SF.v	99545	log plain
-rw-r--r--	Rlimit.v	21174	log plain
-rw-r--r--	Rpower.v	22349	log plain
-rw-r--r--	Rprod.v	6650	log plain
-rw-r--r--	Rseries.v	9675	log plain
-rw-r--r--	Rsigma.v	5084	log plain
-rw-r--r--	Rsqrt_def.v	19743	log plain
-rw-r--r--	Rsyntax.v	8592	log plain
-rw-r--r--	Rtopology.v	68280	log plain
-rw-r--r--	Rtrigo.v	57632	log plain
-rw-r--r--	Rtrigo_alt.v	18389	log plain
-rw-r--r--	Rtrigo_calc.v	14369	log plain
-rw-r--r--	Rtrigo_def.v	14890	log plain
-rw-r--r--	Rtrigo_fun.v	5389	log plain
-rw-r--r--	Rtrigo_reg.v	21319	log plain
-rw-r--r--	SeqProp.v	41280	log plain
-rw-r--r--	SeqSeries.v	8418	log plain
-rw-r--r--	SplitAbsolu.v	900	log plain
-rw-r--r--	SplitRmult.v	759	log plain
-rw-r--r--	Sqrt_reg.v	11960	log plain
-rw-r--r--	TAF.v	23136	log plain
-rw-r--r--	TypeSyntax.v	1223	log plain
-rw-r--r--	intro.tex	122	log plain