ZArith « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	BinInt.v	33452	log plain
-rw-r--r--	Int.v	13961	log plain
-rw-r--r--	Wf_Z.v	8209	log plain
-rw-r--r--	ZArith.v	825	log plain
-rw-r--r--	ZArith_base.v	1282	log plain
-rw-r--r--	ZArith_dec.v	5546	log plain
-rw-r--r--	ZOdiv.v	29834	log plain
-rw-r--r--	ZOdiv_def.v	4860	log plain
-rw-r--r--	Zabs.v	6496	log plain
-rw-r--r--	Zbinary.v	9490	log plain
-rw-r--r--	Zbool.v	6636	log plain
-rw-r--r--	Zcompare.v	18838	log plain
-rw-r--r--	Zcomplements.v	6096	log plain
-rw-r--r--	Zdiv.v	34808	log plain
-rw-r--r--	Zeven.v	9812	log plain
-rw-r--r--	Zgcd_alt.v	9790	log plain
-rw-r--r--	Zhints.v	14164	log plain
-rw-r--r--	Zlogarithm.v	7988	log plain
-rw-r--r--	Zmax.v	4708	log plain
-rw-r--r--	Zmin.v	4374	log plain
-rw-r--r--	Zminmax.v	2519	log plain
-rw-r--r--	Zmisc.v	2895	log plain
-rw-r--r--	Znat.v	8344	log plain
-rw-r--r--	Znumtheory.v	41050	log plain
-rw-r--r--	Zorder.v	29902	log plain
-rw-r--r--	Zpow_def.v	795	log plain
-rw-r--r--	Zpow_facts.v	15130	log plain
-rw-r--r--	Zpower.v	11996	log plain
-rw-r--r--	Zsqrt.v	7223	log plain
-rw-r--r--	Zwf.v	2657	log plain
-rw-r--r--	auxiliary.v	4588	log plain
-rwxr-xr-x	intro.tex	238	log plain