aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
ModeNameSize
-rw-r--r--BinInt.v33074logplain
-rw-r--r--Int.v13961logplain
-rw-r--r--Wf_Z.v8209logplain
-rw-r--r--ZArith.v825logplain
-rw-r--r--ZArith_base.v1282logplain
-rw-r--r--ZArith_dec.v5546logplain
-rw-r--r--ZOdiv.v29834logplain
-rw-r--r--ZOdiv_def.v4860logplain
-rw-r--r--Zabs.v6496logplain
-rw-r--r--Zbinary.v9490logplain
-rw-r--r--Zbool.v6120logplain
-rw-r--r--Zcompare.v18587logplain
-rw-r--r--Zcomplements.v6096logplain
-rw-r--r--Zdiv.v34451logplain
-rw-r--r--Zeven.v9812logplain
-rw-r--r--Zhints.v14164logplain
-rw-r--r--Zlogarithm.v7988logplain
-rw-r--r--Zmax.v4708logplain
-rw-r--r--Zmin.v4374logplain
-rw-r--r--Zminmax.v2519logplain
-rw-r--r--Zmisc.v3288logplain
-rw-r--r--Znat.v8344logplain
-rw-r--r--Znumtheory.v41050logplain
-rw-r--r--Zorder.v29902logplain
-rw-r--r--Zpow_def.v795logplain
-rw-r--r--Zpow_facts.v14612logplain
-rw-r--r--Zpower.v11973logplain
-rw-r--r--Zsqrt.v7223logplain
-rw-r--r--Zwf.v2657logplain
-rw-r--r--auxiliary.v4588logplain
-rwxr-xr-xintro.tex238logplain