ZArith « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	BinInt.v	33793	log plain
-rw-r--r--	Int.v	13483	log plain
-rw-r--r--	Wf_Z.v	8190	log plain
-rw-r--r--	ZArith.v	888	log plain
-rw-r--r--	ZArith_base.v	1269	log plain
-rw-r--r--	ZArith_dec.v	5472	log plain
-rw-r--r--	ZOdiv.v	17150	log plain
-rw-r--r--	ZOdiv_def.v	2049	log plain
-rw-r--r--	Zabs.v	6301	log plain
-rw-r--r--	Zbool.v	6790	log plain
-rw-r--r--	Zcompare.v	20230	log plain
-rw-r--r--	Zcomplements.v	6040	log plain
-rw-r--r--	Zdigits.v	9116	log plain
-rw-r--r--	Zdiv.v	25962	log plain
-rw-r--r--	Zeven.v	9780	log plain
-rw-r--r--	Zgcd_alt.v	9686	log plain
-rw-r--r--	Zhints.v	14072	log plain
-rw-r--r--	Zlogarithm.v	7906	log plain
-rw-r--r--	Zmax.v	3636	log plain
-rw-r--r--	Zmin.v	3076	log plain
-rw-r--r--	Zminmax.v	1183	log plain
-rw-r--r--	Zmisc.v	3070	log plain
-rw-r--r--	Znat.v	8312	log plain
-rw-r--r--	Znumtheory.v	41539	log plain
-rw-r--r--	Zorder.v	30133	log plain
-rw-r--r--	Zpow_def.v	790	log plain
-rw-r--r--	Zpow_facts.v	15054	log plain
-rw-r--r--	Zpower.v	11962	log plain
-rw-r--r--	Zsqrt.v	7209	log plain
-rw-r--r--	Zwf.v	2644	log plain
-rw-r--r--	auxiliary.v	3515	log plain
-rwxr-xr-x	intro.tex	238	log plain
-rw-r--r--	vo.itarget	328	log plain