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

Mode	Name	Size
-rw-r--r--	Alembert.v	28678	log plain
-rw-r--r--	AltSeries.v	16221	log plain
-rw-r--r--	ArithProp.v	7270	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	26885	log plain
-rw-r--r--	Cos_rel.v	11930	log plain
-rw-r--r--	DiscrR.v	2622	log plain
-rw-r--r--	Exp_prop.v	31665	log plain
-rw-r--r--	Integration.v	674	log plain
-rw-r--r--	LegacyRfield.v	1292	log plain
-rw-r--r--	MVT.v	25936	log plain
-rw-r--r--	NewtonInt.v	29572	log plain
-rw-r--r--	PSeries_reg.v	9611	log plain
-rw-r--r--	PartSum.v	20758	log plain
-rw-r--r--	RIneq.v	56864	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	12212	log plain
-rw-r--r--	R_sqrt.v	15325	log plain
-rw-r--r--	Ranalysis.v	29771	log plain
-rw-r--r--	Ranalysis1.v	53596	log plain
-rw-r--r--	Ranalysis2.v	17096	log plain
-rw-r--r--	Ranalysis3.v	30544	log plain
-rw-r--r--	Ranalysis4.v	13202	log plain
-rw-r--r--	Raxioms.v	5187	log plain
-rw-r--r--	Rbase.v	681	log plain
-rw-r--r--	Rbasic_fun.v	18197	log plain
-rw-r--r--	Rcomplete.v	6979	log plain
-rw-r--r--	Rdefinitions.v	2161	log plain
-rw-r--r--	Rderiv.v	22468	log plain
-rw-r--r--	Reals.v	1457	log plain
-rw-r--r--	Rfunctions.v	25633	log plain
-rw-r--r--	Rgeom.v	7919	log plain
-rw-r--r--	RiemannInt.v	140937	log plain
-rw-r--r--	RiemannInt_SF.v	114524	log plain
-rw-r--r--	Rlimit.v	21518	log plain
-rw-r--r--	Rlogic.v	8329	log plain
-rw-r--r--	Rpow_def.v	729	log plain
-rw-r--r--	Rpower.v	24584	log plain
-rw-r--r--	Rprod.v	6675	log plain
-rw-r--r--	Rseries.v	10267	log plain
-rw-r--r--	Rsigma.v	5114	log plain
-rw-r--r--	Rsqrt_def.v	22582	log plain
-rw-r--r--	Rtopology.v	78113	log plain
-rw-r--r--	Rtrigo.v	66450	log plain
-rw-r--r--	Rtrigo_alt.v	17903	log plain
-rw-r--r--	Rtrigo_calc.v	16192	log plain
-rw-r--r--	Rtrigo_def.v	15221	log plain
-rw-r--r--	Rtrigo_fun.v	5364	log plain
-rw-r--r--	Rtrigo_reg.v	23191	log plain
-rw-r--r--	SeqProp.v	43848	log plain
-rw-r--r--	SeqSeries.v	16228	log plain
-rw-r--r--	SplitAbsolu.v	973	log plain
-rw-r--r--	SplitRmult.v	837	log plain
-rw-r--r--	Sqrt_reg.v	13509	log plain
-rw-r--r--	intro.tex	122	log plain