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

Mode	Name	Size
-rw-r--r--	Alembert.v	28666	log plain
-rw-r--r--	AltSeries.v	16200	log plain
-rw-r--r--	ArithProp.v	7252	log plain
-rw-r--r--	Binomial.v	7972	log plain
-rw-r--r--	Cauchy_prod.v	15715	log plain
-rw-r--r--	Cos_plus.v	26824	log plain
-rw-r--r--	Cos_rel.v	11805	log plain
-rw-r--r--	DiscrR.v	2480	log plain
-rw-r--r--	Exp_prop.v	31662	log plain
-rw-r--r--	Integration.v	674	log plain
-rw-r--r--	LegacyRfield.v	1292	log plain
-rw-r--r--	MVT.v	25924	log plain
-rw-r--r--	NewtonInt.v	29565	log plain
-rw-r--r--	PSeries_reg.v	9604	log plain
-rw-r--r--	PartSum.v	20750	log plain
-rw-r--r--	RIneq.v	57811	log plain
-rw-r--r--	RList.v	27853	log plain
-rw-r--r--	ROrderedType.v	2729	log plain
-rw-r--r--	R_Ifp.v	39834	log plain
-rw-r--r--	R_sqr.v	12198	log plain
-rw-r--r--	R_sqrt.v	16256	log plain
-rw-r--r--	Ranalysis.v	29709	log plain
-rw-r--r--	Ranalysis1.v	53569	log plain
-rw-r--r--	Ranalysis2.v	16964	log plain
-rw-r--r--	Ranalysis3.v	30538	log plain
-rw-r--r--	Ranalysis4.v	13189	log plain
-rw-r--r--	Raxioms.v	5173	log plain
-rw-r--r--	Rbase.v	684	log plain
-rw-r--r--	Rbasic_fun.v	21345	log plain
-rw-r--r--	Rcomplete.v	6979	log plain
-rw-r--r--	Rdefinitions.v	2193	log plain
-rw-r--r--	Rderiv.v	22406	log plain
-rw-r--r--	Reals.v	1459	log plain
-rw-r--r--	Rfunctions.v	25829	log plain
-rw-r--r--	Rgeom.v	7916	log plain
-rw-r--r--	RiemannInt.v	140850	log plain
-rw-r--r--	RiemannInt_SF.v	114376	log plain
-rw-r--r--	Rlimit.v	21476	log plain
-rw-r--r--	Rlogic.v	8322	log plain
-rw-r--r--	Rminmax.v	3645	log plain
-rw-r--r--	Rpow_def.v	718	log plain
-rw-r--r--	Rpower.v	24573	log plain
-rw-r--r--	Rprod.v	6652	log plain
-rw-r--r--	Rseries.v	10238	log plain
-rw-r--r--	Rsigma.v	5115	log plain
-rw-r--r--	Rsqrt_def.v	22576	log plain
-rw-r--r--	Rtopology.v	78007	log plain
-rw-r--r--	Rtrigo.v	66387	log plain
-rw-r--r--	Rtrigo_alt.v	17889	log plain
-rw-r--r--	Rtrigo_calc.v	16189	log plain
-rw-r--r--	Rtrigo_def.v	15215	log plain
-rw-r--r--	Rtrigo_fun.v	5356	log plain
-rw-r--r--	Rtrigo_reg.v	23186	log plain
-rw-r--r--	SeqProp.v	43848	log plain
-rw-r--r--	SeqSeries.v	16223	log plain
-rw-r--r--	SplitAbsolu.v	977	log plain
-rw-r--r--	SplitRmult.v	841	log plain
-rw-r--r--	Sqrt_reg.v	13501	log plain
-rw-r--r--	intro.tex	122	log plain
-rw-r--r--	vo.itarget	709	log plain