Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	28629	log plain
-rw-r--r--	AltSeries.v	16171	log plain
-rw-r--r--	ArithProp.v	7221	log plain
-rw-r--r--	Binomial.v	7938	log plain
-rw-r--r--	Cauchy_prod.v	15679	log plain
-rw-r--r--	Cos_plus.v	26836	log plain
-rw-r--r--	Cos_rel.v	11882	log plain
-rw-r--r--	DiscrR.v	2575	log plain
-rw-r--r--	Exp_prop.v	31616	log plain
-rw-r--r--	Integration.v	623	log plain
-rw-r--r--	LegacyRfield.v	1239	log plain
-rw-r--r--	MVT.v	25892	log plain
-rw-r--r--	NewtonInt.v	29522	log plain
-rw-r--r--	PSeries_reg.v	9559	log plain
-rw-r--r--	PartSum.v	20710	log plain
-rw-r--r--	RIneq.v	50139	log plain
-rw-r--r--	RList.v	27910	log plain
-rw-r--r--	R_Ifp.v	39851	log plain
-rw-r--r--	R_sqr.v	12166	log plain
-rw-r--r--	R_sqrt.v	15278	log plain
-rw-r--r--	Ranalysis.v	29721	log plain
-rw-r--r--	Ranalysis1.v	53545	log plain
-rw-r--r--	Ranalysis2.v	17045	log plain
-rw-r--r--	Ranalysis3.v	30493	log plain
-rw-r--r--	Ranalysis4.v	13151	log plain
-rw-r--r--	Raxioms.v	5139	log plain
-rw-r--r--	Rbase.v	638	log plain
-rw-r--r--	Rbasic_fun.v	18146	log plain
-rw-r--r--	Rcomplete.v	6929	log plain
-rw-r--r--	Rdefinitions.v	2118	log plain
-rw-r--r--	Rderiv.v	22421	log plain
-rw-r--r--	Reals.v	1415	log plain
-rw-r--r--	Rfunctions.v	25606	log plain
-rw-r--r--	Rgeom.v	7873	log plain
-rw-r--r--	RiemannInt.v	140886	log plain
-rw-r--r--	RiemannInt_SF.v	114470	log plain
-rw-r--r--	Rlimit.v	21471	log plain
-rw-r--r--	Rlogic.v	6608	log plain
-rw-r--r--	Rpow_def.v	142	log plain
-rw-r--r--	Rpower.v	24537	log plain
-rw-r--r--	Rprod.v	6629	log plain
-rw-r--r--	Rseries.v	10219	log plain
-rw-r--r--	Rsigma.v	5068	log plain
-rw-r--r--	Rsqrt_def.v	22532	log plain
-rw-r--r--	Rtopology.v	78063	log plain
-rw-r--r--	Rtrigo.v	66404	log plain
-rw-r--r--	Rtrigo_alt.v	17852	log plain
-rw-r--r--	Rtrigo_calc.v	16144	log plain
-rw-r--r--	Rtrigo_def.v	15170	log plain
-rw-r--r--	Rtrigo_fun.v	5313	log plain
-rw-r--r--	Rtrigo_reg.v	23140	log plain
-rw-r--r--	SeqProp.v	43800	log plain
-rw-r--r--	SeqSeries.v	16178	log plain
-rw-r--r--	SplitAbsolu.v	925	log plain
-rw-r--r--	SplitRmult.v	790	log plain
-rw-r--r--	Sqrt_reg.v	13460	log plain
-rw-r--r--	intro.tex	122	log plain