Reals « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Alembert.v	27447	log plain
-rw-r--r--	AltSeries.v	14384	log plain
-rw-r--r--	ArithProp.v	6989	log plain
-rw-r--r--	Binomial.v	7516	log plain
-rw-r--r--	Cauchy_prod.v	15543	log plain
-rw-r--r--	Cos_plus.v	25899	log plain
-rw-r--r--	Cos_rel.v	10540	log plain
-rw-r--r--	DiscrR.v	2034	log plain
-rw-r--r--	Exp_prop.v	30106	log plain
-rw-r--r--	Integration.v	609	log plain
-rw-r--r--	MVT.v	26479	log plain
-rw-r--r--	Machin.v	6642	log plain
-rw-r--r--	NewtonInt.v	27593	log plain
-rw-r--r--	PSeries_reg.v	24858	log plain
-rw-r--r--	PartSum.v	19993	log plain
-rw-r--r--	RIneq.v	58276	log plain
-rw-r--r--	RList.v	26767	log plain
-rw-r--r--	ROrderedType.v	2737	log plain
-rw-r--r--	R_Ifp.v	37805	log plain
-rw-r--r--	R_sqr.v	10503	log plain
-rw-r--r--	R_sqrt.v	12374	log plain
-rw-r--r--	Ranalysis.v	1057	log plain
-rw-r--r--	Ranalysis1.v	53845	log plain
-rw-r--r--	Ranalysis2.v	16027	log plain
-rw-r--r--	Ranalysis3.v	29406	log plain
-rw-r--r--	Ranalysis4.v	12863	log plain
-rw-r--r--	Ranalysis5.v	55533	log plain
-rw-r--r--	Ranalysis_reg.v	30125	log plain
-rw-r--r--	Ratan.v	60945	log plain
-rw-r--r--	Raxioms.v	4722	log plain
-rw-r--r--	Rbase.v	624	log plain
-rw-r--r--	Rbasic_fun.v	21320	log plain
-rw-r--r--	Rcomplete.v	6698	log plain
-rw-r--r--	Rdefinitions.v	2802	log plain
-rw-r--r--	Rderiv.v	21457	log plain
-rw-r--r--	Reals.v	1400	log plain
-rw-r--r--	Rfunctions.v	27145	log plain
-rw-r--r--	Rgeom.v	7745	log plain
-rw-r--r--	RiemannInt.v	136009	log plain
-rw-r--r--	RiemannInt_SF.v	108369	log plain
-rw-r--r--	Rlimit.v	20042	log plain
-rw-r--r--	Rlogic.v	5543	log plain
-rw-r--r--	Rminmax.v	3645	log plain
-rw-r--r--	Rpow_def.v	656	log plain
-rw-r--r--	Rpower.v	28522	log plain
-rw-r--r--	Rprod.v	6536	log plain
-rw-r--r--	Rseries.v	13318	log plain
-rw-r--r--	Rsigma.v	4940	log plain
-rw-r--r--	Rsqrt_def.v	21590	log plain
-rw-r--r--	Rtopology.v	73237	log plain
-rw-r--r--	Rtrigo.v	963	log plain
-rw-r--r--	Rtrigo1.v	65247	log plain
-rw-r--r--	Rtrigo_alt.v	15462	log plain
-rw-r--r--	Rtrigo_calc.v	11120	log plain
-rw-r--r--	Rtrigo_def.v	13941	log plain
-rw-r--r--	Rtrigo_fun.v	5388	log plain
-rw-r--r--	Rtrigo_reg.v	16429	log plain
-rw-r--r--	SeqProp.v	37471	log plain
-rw-r--r--	SeqSeries.v	15782	log plain
-rw-r--r--	SplitAbsolu.v	911	log plain
-rw-r--r--	SplitRmult.v	776	log plain
-rw-r--r--	Sqrt_reg.v	12729	log plain