summaryrefslogtreecommitdiff
path: root/theories/ZArith
ModeNameSize
-rw-r--r--BinInt.v31267logplain
-rw-r--r--Wf_Z.v7781logplain
-rw-r--r--ZArith.v851logplain
-rw-r--r--ZArith_base.v1333logplain
-rw-r--r--ZArith_dec.v5271logplain
-rw-r--r--Zabs.v4293logplain
-rw-r--r--Zbinary.v10236logplain
-rw-r--r--Zbool.v5769logplain
-rw-r--r--Zcompare.v19120logplain
-rw-r--r--Zcomplements.v5881logplain
-rw-r--r--Zdiv.v10646logplain
-rw-r--r--Zeven.v6250logplain
-rw-r--r--Zhints.v13556logplain
-rw-r--r--Zlogarithm.v8190logplain
-rw-r--r--Zmax.v3151logplain
-rw-r--r--Zmin.v3977logplain
-rw-r--r--Zminmax.v2528logplain
-rw-r--r--Zmisc.v3265logplain
-rw-r--r--Znat.v4744logplain
-rw-r--r--Znumtheory.v18296logplain
-rw-r--r--Zorder.v28095logplain
-rw-r--r--Zpower.v12168logplain
-rw-r--r--Zsqrt.v5465logplain
-rw-r--r--Zwf.v2564logplain
-rw-r--r--auxiliary.v4492logplain
-rwxr-xr-xintro.tex238logplain