Reals « theories - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Alembert.v	27597	log plain
-rw-r--r--	AltSeries.v	14534	log plain
-rw-r--r--	ArithProp.v	7139	log plain
-rw-r--r--	Binomial.v	7666	log plain
-rw-r--r--	Cauchy_prod.v	15693	log plain
-rw-r--r--	ClassicalDedekindReals.v	20825	log plain
-rw-r--r--	ConstructiveCauchyReals.v	53221	log plain
-rw-r--r--	ConstructiveCauchyRealsMult.v	65098	log plain
-rw-r--r--	ConstructiveRcomplete.v	17079	log plain
-rw-r--r--	ConstructiveReals.v	34076	log plain
-rw-r--r--	ConstructiveRealsLUB.v	13304	log plain
-rw-r--r--	ConstructiveRealsMorphisms.v	55873	log plain
-rw-r--r--	Cos_plus.v	26023	log plain
-rw-r--r--	Cos_rel.v	10674	log plain
-rw-r--r--	DiscrR.v	2180	log plain
-rw-r--r--	Exp_prop.v	30244	log plain
-rw-r--r--	Integration.v	759	log plain
-rw-r--r--	MVT.v	26629	log plain
-rw-r--r--	Machin.v	6690	log plain
-rw-r--r--	NewtonInt.v	27743	log plain
-rw-r--r--	PSeries_reg.v	24880	log plain
-rw-r--r--	PartSum.v	20143	log plain
-rw-r--r--	RIneq.v	58776	log plain
-rw-r--r--	RList.v	26917	log plain
-rw-r--r--	ROrderedType.v	2887	log plain
-rw-r--r--	R_Ifp.v	37922	log plain
-rw-r--r--	R_sqr.v	10653	log plain
-rw-r--r--	R_sqrt.v	12889	log plain
-rw-r--r--	Ranalysis.v	1207	log plain
-rw-r--r--	Ranalysis1.v	54021	log plain
-rw-r--r--	Ranalysis2.v	16155	log plain
-rw-r--r--	Ranalysis3.v	29556	log plain
-rw-r--r--	Ranalysis4.v	13013	log plain
-rw-r--r--	Ranalysis5.v	54787	log plain
-rw-r--r--	Ranalysis_reg.v	30275	log plain
-rw-r--r--	Ratan.v	60443	log plain
-rw-r--r--	Raxioms.v	16419	log plain
-rw-r--r--	Rbase.v	774	log plain
-rw-r--r--	Rbasic_fun.v	21553	log plain
-rw-r--r--	Rcomplete.v	6848	log plain
-rw-r--r--	Rdefinitions.v	7319	log plain
-rw-r--r--	Rderiv.v	21591	log plain
-rw-r--r--	Reals.v	1574	log plain
-rw-r--r--	Rfunctions.v	27281	log plain
-rw-r--r--	Rgeom.v	7895	log plain
-rw-r--r--	RiemannInt.v	136159	log plain
-rw-r--r--	RiemannInt_SF.v	108519	log plain
-rw-r--r--	Rlimit.v	20176	log plain
-rw-r--r--	Rlogic.v	5693	log plain
-rw-r--r--	Rminmax.v	3795	log plain
-rw-r--r--	Rpow_def.v	806	log plain
-rw-r--r--	Rpower.v	28624	log plain
-rw-r--r--	Rprod.v	6644	log plain
-rw-r--r--	Rseries.v	13468	log plain
-rw-r--r--	Rsigma.v	5080	log plain
-rw-r--r--	Rsqrt_def.v	21741	log plain
-rw-r--r--	Rtopology.v	73387	log plain
-rw-r--r--	Rtrigo.v	1109	log plain
-rw-r--r--	Rtrigo1.v	65335	log plain
-rw-r--r--	Rtrigo_alt.v	15612	log plain
-rw-r--r--	Rtrigo_calc.v	11438	log plain
-rw-r--r--	Rtrigo_def.v	14091	log plain
-rw-r--r--	Rtrigo_fun.v	5538	log plain
-rw-r--r--	Rtrigo_reg.v	16579	log plain
-rw-r--r--	Runcountable.v	19824	log plain
-rw-r--r--	SeqProp.v	37617	log plain
-rw-r--r--	SeqSeries.v	15932	log plain
-rw-r--r--	SplitAbsolu.v	1061	log plain
-rw-r--r--	SplitRmult.v	926	log plain
-rw-r--r--	Sqrt_reg.v	12879	log plain