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

Mode	Name	Size
-rw-r--r--	Alembert.v	28617	log plain
-rw-r--r--	AltSeries.v	16150	log plain
-rw-r--r--	ArithProp.v	7202	log plain
-rw-r--r--	Binomial.v	7923	log plain
-rw-r--r--	Cauchy_prod.v	15663	log plain
-rw-r--r--	Cos_plus.v	26775	log plain
-rw-r--r--	Cos_rel.v	11757	log plain
-rw-r--r--	DiscrR.v	2433	log plain
-rw-r--r--	Exp_prop.v	31613	log plain
-rw-r--r--	Integration.v	622	log plain
-rw-r--r--	LegacyRfield.v	1239	log plain
-rw-r--r--	MVT.v	25880	log plain
-rw-r--r--	NewtonInt.v	29515	log plain
-rw-r--r--	PSeries_reg.v	9552	log plain
-rw-r--r--	PartSum.v	20702	log plain
-rw-r--r--	RIneq.v	57765	log plain
-rw-r--r--	RList.v	27807	log plain
-rw-r--r--	ROrderedType.v	2729	log plain
-rw-r--r--	R_Ifp.v	39788	log plain
-rw-r--r--	R_sqr.v	12152	log plain
-rw-r--r--	R_sqrt.v	16209	log plain
-rw-r--r--	Ranalysis.v	29659	log plain
-rw-r--r--	Ranalysis1.v	53518	log plain
-rw-r--r--	Ranalysis2.v	16913	log plain
-rw-r--r--	Ranalysis3.v	30487	log plain
-rw-r--r--	Ranalysis4.v	13138	log plain
-rw-r--r--	Raxioms.v	5125	log plain
-rw-r--r--	Rbase.v	638	log plain
-rw-r--r--	Rbasic_fun.v	21294	log plain
-rw-r--r--	Rcomplete.v	6929	log plain
-rw-r--r--	Rdefinitions.v	2140	log plain
-rw-r--r--	Rderiv.v	22359	log plain
-rw-r--r--	Reals.v	1413	log plain
-rw-r--r--	Rfunctions.v	25778	log plain
-rw-r--r--	Rgeom.v	7870	log plain
-rw-r--r--	RiemannInt.v	140799	log plain
-rw-r--r--	RiemannInt_SF.v	114322	log plain
-rw-r--r--	Rlimit.v	21429	log plain
-rw-r--r--	Rlogic.v	8322	log plain
-rw-r--r--	Rminmax.v	3645	log plain
-rw-r--r--	Rpow_def.v	669	log plain
-rw-r--r--	Rpower.v	24526	log plain
-rw-r--r--	Rprod.v	6606	log plain
-rw-r--r--	Rseries.v	10190	log plain
-rw-r--r--	Rsigma.v	5068	log plain
-rw-r--r--	Rsqrt_def.v	22526	log plain
-rw-r--r--	Rtopology.v	77957	log plain
-rw-r--r--	Rtrigo.v	66340	log plain
-rw-r--r--	Rtrigo_alt.v	17838	log plain
-rw-r--r--	Rtrigo_calc.v	16137	log plain
-rw-r--r--	Rtrigo_def.v	15164	log plain
-rw-r--r--	Rtrigo_fun.v	5305	log plain
-rw-r--r--	Rtrigo_reg.v	23135	log plain
-rw-r--r--	SeqProp.v	43800	log plain
-rw-r--r--	SeqSeries.v	16173	log plain
-rw-r--r--	SplitAbsolu.v	925	log plain
-rw-r--r--	SplitRmult.v	790	log plain
-rw-r--r--	Sqrt_reg.v	13452	log plain
-rw-r--r--	intro.tex	122	log plain
-rw-r--r--	vo.itarget	709	log plain