summaryrefslogtreecommitdiff
path: root/theories/ZArith
ModeNameSize
-rw-r--r--BinInt.v51967logplain
-rw-r--r--BinIntDef.v14879logplain
-rw-r--r--Int.v13357logplain
-rw-r--r--Wf_Z.v6003logplain
-rw-r--r--ZArith.v841logplain
-rw-r--r--ZArith_base.v1302logplain
-rw-r--r--ZArith_dec.v4801logplain
-rw-r--r--ZOdiv.v4567logplain
-rw-r--r--ZOdiv_def.v726logplain
-rw-r--r--Zabs.v3577logplain
-rw-r--r--Zbool.v4876logplain
-rw-r--r--Zcompare.v5519logplain
-rw-r--r--Zcomplements.v4776logplain
-rw-r--r--Zdigits.v8846logplain
-rw-r--r--Zdiv.v21332logplain
-rw-r--r--Zeuclid.v1734logplain
-rw-r--r--Zeven.v7865logplain
-rw-r--r--Zgcd_alt.v9185logplain
-rw-r--r--Zhints.v3916logplain
-rw-r--r--Zlogarithm.v8430logplain
-rw-r--r--Zmax.v2448logplain
-rw-r--r--Zmin.v2218logplain
-rw-r--r--Zminmax.v1151logplain
-rw-r--r--Zmisc.v1077logplain
-rw-r--r--Znat.v27576logplain
-rw-r--r--Znumtheory.v26681logplain
-rw-r--r--Zorder.v15215logplain
-rw-r--r--Zpow_alt.v2561logplain
-rw-r--r--Zpow_def.v1332logplain
-rw-r--r--Zpow_facts.v8056logplain
-rw-r--r--Zpower.v9555logplain
-rw-r--r--Zquot.v14360logplain
-rw-r--r--Zsqrt_compat.v7686logplain
-rw-r--r--Zwf.v2526logplain
-rw-r--r--auxiliary.v2397logplain
-rwxr-xr-xintro.tex238logplain
-rw-r--r--vo.itarget380logplain