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

Mode	Name	Size
-rw-r--r--	Alembert.v	25974	log plain
-rw-r--r--	AltSeries.v	15715	log plain
-rw-r--r--	ArithProp.v	6372	log plain
-rw-r--r--	Binomial.v	7368	log plain
-rw-r--r--	Cauchy_prod.v	14162	log plain
-rw-r--r--	Cos_plus.v	32956	log plain
-rw-r--r--	Cos_rel.v	14079	log plain
-rw-r--r--	DiscrR.v	2784	log plain
-rw-r--r--	Exp_prop.v	30243	log plain
-rw-r--r--	Integration.v	682	log plain
-rw-r--r--	MVT.v	23246	log plain
-rw-r--r--	NewtonInt.v	27097	log plain
-rw-r--r--	PSeries_reg.v	8653	log plain
-rw-r--r--	PartSum.v	18408	log plain
-rw-r--r--	RIneq.v	45888	log plain
-rw-r--r--	RList.v	22699	log plain
-rw-r--r--	R_Ifp.v	27097	log plain
-rw-r--r--	R_sqr.v	10916	log plain
-rw-r--r--	R_sqrt.v	13209	log plain
-rw-r--r--	Ranalysis.v	23767	log plain
-rw-r--r--	Ranalysis1.v	46440	log plain
-rw-r--r--	Ranalysis2.v	16094	log plain
-rw-r--r--	Ranalysis3.v	27830	log plain
-rw-r--r--	Ranalysis4.v	11794	log plain
-rw-r--r--	Raxioms.v	5787	log plain
-rw-r--r--	Rbase.v	691	log plain
-rw-r--r--	Rbasic_fun.v	17557	log plain
-rw-r--r--	Rcomplete.v	6513	log plain
-rw-r--r--	Rdefinitions.v	2197	log plain
-rw-r--r--	Rderiv.v	20837	log plain
-rw-r--r--	Reals.v	1468	log plain
-rw-r--r--	Rfunctions.v	25169	log plain
-rw-r--r--	Rgeom.v	6612	log plain
-rw-r--r--	RiemannInt.v	125014	log plain
-rw-r--r--	RiemannInt_SF.v	99802	log plain
-rw-r--r--	Rlimit.v	21287	log plain
-rw-r--r--	Rpower.v	22460	log plain
-rw-r--r--	Rprod.v	6800	log plain
-rw-r--r--	Rseries.v	9854	log plain
-rw-r--r--	Rsigma.v	5233	log plain
-rw-r--r--	Rsqrt_def.v	19790	log plain
-rw-r--r--	Rsyntax.v	8670	log plain
-rw-r--r--	Rtopology.v	67466	log plain
-rw-r--r--	Rtrigo.v	57532	log plain
-rw-r--r--	Rtrigo_alt.v	18329	log plain
-rw-r--r--	Rtrigo_calc.v	13884	log plain
-rw-r--r--	Rtrigo_def.v	14887	log plain
-rw-r--r--	Rtrigo_fun.v	5542	log plain
-rw-r--r--	Rtrigo_reg.v	21505	log plain
-rw-r--r--	SeqProp.v	39610	log plain
-rw-r--r--	SeqSeries.v	14551	log plain
-rw-r--r--	SplitAbsolu.v	986	log plain
-rw-r--r--	SplitRmult.v	834	log plain
-rw-r--r--	Sqrt_reg.v	12075	log plain