Reals « theories - debian-coq - Debian packaging for Coq

Mode	Name	Size
-rw-r--r--	Alembert.v	27392	log plain
-rw-r--r--	AltSeries.v	15849	log plain
-rw-r--r--	ArithProp.v	6858	log plain
-rw-r--r--	Binomial.v	7582	log plain
-rw-r--r--	Cauchy_prod.v	14838	log plain
-rw-r--r--	Cos_plus.v	31885	log plain
-rw-r--r--	Cos_rel.v	13012	log plain
-rw-r--r--	DiscrR.v	3044	log plain
-rw-r--r--	Exp_prop.v	31422	log plain
-rw-r--r--	Integration.v	682	log plain
-rw-r--r--	MVT.v	24548	log plain
-rw-r--r--	NewtonInt.v	28127	log plain
-rw-r--r--	PSeries_reg.v	9315	log plain
-rw-r--r--	PartSum.v	19687	log plain
-rw-r--r--	RIneq.v	47499	log plain
-rw-r--r--	RList.v	26120	log plain
-rw-r--r--	R_Ifp.v	25367	log plain
-rw-r--r--	R_sqr.v	11302	log plain
-rw-r--r--	R_sqrt.v	14377	log plain
-rw-r--r--	Ranalysis.v	28570	log plain
-rw-r--r--	Ranalysis1.v	49801	log plain
-rw-r--r--	Ranalysis2.v	16309	log plain
-rw-r--r--	Ranalysis3.v	28782	log plain
-rw-r--r--	Ranalysis4.v	12491	log plain
-rw-r--r--	Raxioms.v	5197	log plain
-rw-r--r--	Rbase.v	691	log plain
-rw-r--r--	Rbasic_fun.v	17121	log plain
-rw-r--r--	Rcomplete.v	6647	log plain
-rw-r--r--	Rdefinitions.v	2224	log plain
-rw-r--r--	Rderiv.v	18481	log plain
-rw-r--r--	Reals.v	1468	log plain
-rw-r--r--	Rfunctions.v	24828	log plain
-rw-r--r--	Rgeom.v	7564	log plain
-rw-r--r--	RiemannInt.v	132277	log plain
-rw-r--r--	RiemannInt_SF.v	108310	log plain
-rw-r--r--	Rlimit.v	19933	log plain
-rw-r--r--	Rpower.v	22751	log plain
-rw-r--r--	Rprod.v	7200	log plain
-rw-r--r--	Rseries.v	9363	log plain
-rw-r--r--	Rsigma.v	5374	log plain
-rw-r--r--	Rsqrt_def.v	21263	log plain
-rw-r--r--	Rtopology.v	73296	log plain
-rw-r--r--	Rtrigo.v	61361	log plain
-rw-r--r--	Rtrigo_alt.v	17946	log plain
-rw-r--r--	Rtrigo_calc.v	15259	log plain
-rw-r--r--	Rtrigo_def.v	14582	log plain
-rw-r--r--	Rtrigo_fun.v	5209	log plain
-rw-r--r--	Rtrigo_reg.v	22210	log plain
-rw-r--r--	SeqProp.v	41746	log plain
-rw-r--r--	SeqSeries.v	15494	log plain
-rw-r--r--	SplitAbsolu.v	977	log plain
-rw-r--r--	SplitRmult.v	846	log plain
-rw-r--r--	Sqrt_reg.v	12800	log plain
-rw-r--r--	intro.tex	122	log plain