ZArith « theories - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	BinInt.v	52922	log plain
-rw-r--r--	BinIntDef.v	16482	log plain
-rw-r--r--	Int.v	15392	log plain
-rw-r--r--	Wf_Z.v	6246	log plain
-rw-r--r--	ZArith.v	1035	log plain
-rw-r--r--	ZArith_base.v	1462	log plain
-rw-r--r--	ZArith_dec.v	4882	log plain
-rw-r--r--	Zabs.v	3533	log plain
-rw-r--r--	Zbool.v	5026	log plain
-rw-r--r--	Zcompare.v	5338	log plain
-rw-r--r--	Zcomplements.v	5496	log plain
-rw-r--r--	Zdigits.v	8971	log plain
-rw-r--r--	Zdiv.v	22403	log plain
-rw-r--r--	Zeuclid.v	1884	log plain
-rw-r--r--	Zeven.v	7946	log plain
-rw-r--r--	Zgcd_alt.v	8948	log plain
-rw-r--r--	Zhints.v	4076	log plain
-rw-r--r--	Zmax.v	2127	log plain
-rw-r--r--	Zmin.v	1897	log plain
-rw-r--r--	Zminmax.v	1301	log plain
-rw-r--r--	Zmisc.v	1227	log plain
-rw-r--r--	Znat.v	27894	log plain
-rw-r--r--	Znumtheory.v	30215	log plain
-rw-r--r--	Zorder.v	14819	log plain
-rw-r--r--	Zpow_alt.v	2711	log plain
-rw-r--r--	Zpow_def.v	1512	log plain
-rw-r--r--	Zpow_facts.v	8069	log plain
-rw-r--r--	Zpower.v	10988	log plain
-rw-r--r--	Zquot.v	13750	log plain
-rw-r--r--	Zwf.v	2485	log plain
-rw-r--r--	auxiliary.v	2546	log plain