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

Mode	Name	Size
-rw-r--r--	Alembert.v	27398	log plain
-rw-r--r--	AltSeries.v	15840	log plain
-rw-r--r--	ArithProp.v	6849	log plain
-rw-r--r--	Binomial.v	7575	log plain
-rw-r--r--	Cauchy_prod.v	14829	log plain
-rw-r--r--	Cos_plus.v	31876	log plain
-rw-r--r--	Cos_rel.v	13002	log plain
-rw-r--r--	DiscrR.v	3035	log plain
-rw-r--r--	Exp_prop.v	31416	log plain
-rw-r--r--	Integration.v	674	log plain
-rw-r--r--	MVT.v	24559	log plain
-rw-r--r--	NewtonInt.v	28134	log plain
-rw-r--r--	PSeries_reg.v	9306	log plain
-rw-r--r--	PartSum.v	19683	log plain
-rw-r--r--	RIneq.v	47490	log plain
-rw-r--r--	RList.v	26111	log plain
-rw-r--r--	R_Ifp.v	25358	log plain
-rw-r--r--	R_sqr.v	11293	log plain
-rw-r--r--	R_sqrt.v	14369	log plain
-rw-r--r--	Ranalysis.v	28561	log plain
-rw-r--r--	Ranalysis1.v	49937	log plain
-rw-r--r--	Ranalysis2.v	16300	log plain
-rw-r--r--	Ranalysis3.v	28828	log plain
-rw-r--r--	Ranalysis4.v	12505	log plain
-rw-r--r--	Raxioms.v	5194	log plain
-rw-r--r--	Rbase.v	682	log plain
-rw-r--r--	Rbasic_fun.v	17112	log plain
-rw-r--r--	Rcomplete.v	6638	log plain
-rw-r--r--	Rdefinitions.v	2215	log plain
-rw-r--r--	Rderiv.v	18472	log plain
-rw-r--r--	Reals.v	1459	log plain
-rw-r--r--	Rfunctions.v	24831	log plain
-rw-r--r--	Rgeom.v	7555	log plain
-rw-r--r--	RiemannInt.v	132268	log plain
-rw-r--r--	RiemannInt_SF.v	108307	log plain
-rw-r--r--	Rlimit.v	19924	log plain
-rw-r--r--	Rpower.v	22743	log plain
-rw-r--r--	Rprod.v	7198	log plain
-rw-r--r--	Rseries.v	9360	log plain
-rw-r--r--	Rsigma.v	5365	log plain
-rw-r--r--	Rsqrt_def.v	21266	log plain
-rw-r--r--	Rtopology.v	73287	log plain
-rw-r--r--	Rtrigo.v	61351	log plain
-rw-r--r--	Rtrigo_alt.v	17936	log plain
-rw-r--r--	Rtrigo_calc.v	15250	log plain
-rw-r--r--	Rtrigo_def.v	14574	log plain
-rw-r--r--	Rtrigo_fun.v	5157	log plain
-rw-r--r--	Rtrigo_reg.v	22206	log plain
-rw-r--r--	SeqProp.v	41563	log plain
-rw-r--r--	SeqSeries.v	15500	log plain
-rw-r--r--	SplitAbsolu.v	969	log plain
-rw-r--r--	SplitRmult.v	838	log plain
-rw-r--r--	Sqrt_reg.v	12792	log plain
-rw-r--r--	intro.tex	122	log plain