ZArith « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	BinInt.v	52537	log plain
-rw-r--r--	BinIntDef.v	15437	log plain
-rw-r--r--	Int.v	15359	log plain
-rw-r--r--	Wf_Z.v	6190	log plain
-rw-r--r--	ZArith.v	991	log plain
-rw-r--r--	ZArith_base.v	1452	log plain
-rw-r--r--	ZArith_dec.v	4951	log plain
-rw-r--r--	Zabs.v	3727	log plain
-rw-r--r--	Zbool.v	5026	log plain
-rw-r--r--	Zcompare.v	5669	log plain
-rw-r--r--	Zcomplements.v	4890	log plain
-rw-r--r--	Zdigits.v	9008	log plain
-rw-r--r--	Zdiv.v	21570	log plain
-rw-r--r--	Zeuclid.v	1884	log plain
-rw-r--r--	Zeven.v	8021	log plain
-rw-r--r--	Zgcd_alt.v	9359	log plain
-rw-r--r--	Zhints.v	4066	log plain
-rw-r--r--	Zlogarithm.v	8588	log plain
-rw-r--r--	Zmax.v	2598	log plain
-rw-r--r--	Zmin.v	2368	log plain
-rw-r--r--	Zminmax.v	1301	log plain
-rw-r--r--	Zmisc.v	1227	log plain
-rw-r--r--	Znat.v	27713	log plain
-rw-r--r--	Znumtheory.v	26836	log plain
-rw-r--r--	Zorder.v	15424	log plain
-rw-r--r--	Zpow_alt.v	2711	log plain
-rw-r--r--	Zpow_def.v	1482	log plain
-rw-r--r--	Zpow_facts.v	8161	log plain
-rw-r--r--	Zpower.v	9694	log plain
-rw-r--r--	Zquot.v	14509	log plain
-rw-r--r--	Zsqrt_compat.v	7853	log plain
-rw-r--r--	Zwf.v	2668	log plain
-rw-r--r--	auxiliary.v	2547	log plain