summaryrefslogtreecommitdiff
path: root/theories/ZArith
ModeNameSize
-rw-r--r--BinInt.v45877logplain
-rw-r--r--BinIntDef.v14942logplain
-rw-r--r--Int.v13430logplain
-rw-r--r--Wf_Z.v6000logplain
-rw-r--r--ZArith.v841logplain
-rw-r--r--ZArith_base.v1302logplain
-rw-r--r--ZArith_dec.v5354logplain
-rw-r--r--ZOdiv.v4567logplain
-rw-r--r--ZOdiv_def.v726logplain
-rw-r--r--Zabs.v3572logplain
-rw-r--r--Zbool.v4876logplain
-rw-r--r--Zcompare.v5518logplain
-rw-r--r--Zcomplements.v4767logplain
-rw-r--r--Zdigits.v9105logplain
-rw-r--r--Zdiv.v21279logplain
-rw-r--r--Zeuclid.v1734logplain
-rw-r--r--Zeven.v7885logplain
-rw-r--r--Zgcd_alt.v9688logplain
-rw-r--r--Zhints.v4208logplain
-rw-r--r--Zlogarithm.v8732logplain
-rw-r--r--Zmax.v3372logplain
-rw-r--r--Zmin.v2899logplain
-rw-r--r--Zminmax.v1151logplain
-rw-r--r--Zmisc.v1067logplain
-rw-r--r--Znat.v26852logplain
-rw-r--r--Znumtheory.v27906logplain
-rw-r--r--Zorder.v15184logplain
-rw-r--r--Zpow_alt.v2558logplain
-rw-r--r--Zpow_def.v1329logplain
-rw-r--r--Zpow_facts.v8049logplain
-rw-r--r--Zpower.v9541logplain
-rw-r--r--Zquot.v16143logplain
-rw-r--r--Zsqrt_compat.v7835logplain
-rw-r--r--Zwf.v2644logplain
-rw-r--r--auxiliary.v2397logplain
-rwxr-xr-xintro.tex238logplain
-rw-r--r--vo.itarget380logplain