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

Mode	Name	Size
-rw-r--r--	Alembert.v	28917	log plain
-rw-r--r--	AltSeries.v	16329	log plain
-rw-r--r--	ArithProp.v	7268	log plain
-rw-r--r--	Binomial.v	7983	log plain
-rw-r--r--	Cauchy_prod.v	15727	log plain
-rw-r--r--	Cos_plus.v	26889	log plain
-rw-r--r--	Cos_rel.v	12071	log plain
-rw-r--r--	DiscrR.v	2619	log plain
-rw-r--r--	Exp_prop.v	31751	log plain
-rw-r--r--	Integration.v	674	log plain
-rw-r--r--	LegacyRfield.v	1239	log plain
-rw-r--r--	MVT.v	25965	log plain
-rw-r--r--	NewtonInt.v	29763	log plain
-rw-r--r--	PSeries_reg.v	9728	log plain
-rw-r--r--	PartSum.v	20770	log plain
-rw-r--r--	RIneq.v	49264	log plain
-rw-r--r--	RList.v	27952	log plain
-rw-r--r--	R_Ifp.v	39893	log plain
-rw-r--r--	R_sqr.v	12208	log plain
-rw-r--r--	R_sqrt.v	15321	log plain
-rw-r--r--	Ranalysis.v	29768	log plain
-rw-r--r--	Ranalysis1.v	53644	log plain
-rw-r--r--	Ranalysis2.v	17092	log plain
-rw-r--r--	Ranalysis3.v	30556	log plain
-rw-r--r--	Ranalysis4.v	13286	log plain
-rw-r--r--	Raxioms.v	5191	log plain
-rw-r--r--	Rbase.v	681	log plain
-rw-r--r--	Rbasic_fun.v	18193	log plain
-rw-r--r--	Rcomplete.v	6993	log plain
-rw-r--r--	Rdefinitions.v	2153	log plain
-rw-r--r--	Rderiv.v	22464	log plain
-rw-r--r--	Reals.v	1457	log plain
-rw-r--r--	Rfunctions.v	25702	log plain
-rw-r--r--	Rgeom.v	7915	log plain
-rw-r--r--	RiemannInt.v	141086	log plain
-rw-r--r--	RiemannInt_SF.v	114945	log plain
-rw-r--r--	Rlimit.v	21496	log plain
-rw-r--r--	Rpower.v	24075	log plain
-rw-r--r--	Rprod.v	5893	log plain
-rw-r--r--	Rseries.v	10261	log plain
-rw-r--r--	Rsigma.v	5119	log plain
-rw-r--r--	Rsqrt_def.v	22737	log plain
-rw-r--r--	Rtopology.v	78110	log plain
-rw-r--r--	Rtrigo.v	66390	log plain
-rw-r--r--	Rtrigo_alt.v	17905	log plain
-rw-r--r--	Rtrigo_calc.v	16192	log plain
-rw-r--r--	Rtrigo_def.v	15303	log plain
-rw-r--r--	Rtrigo_fun.v	5428	log plain
-rw-r--r--	Rtrigo_reg.v	23307	log plain
-rw-r--r--	SeqProp.v	43854	log plain
-rw-r--r--	SeqSeries.v	16346	log plain
-rw-r--r--	SplitAbsolu.v	973	log plain
-rw-r--r--	SplitRmult.v	837	log plain
-rw-r--r--	Sqrt_reg.v	13515	log plain
-rw-r--r--	intro.tex	122	log plain