summaryrefslogtreecommitdiff
path: root/theories/ZArith
ModeNameSize
-rw-r--r--BinInt.v33559logplain
-rw-r--r--Int.v13539logplain
-rw-r--r--Wf_Z.v8249logplain
-rw-r--r--ZArith.v872logplain
-rw-r--r--ZArith_base.v1333logplain
-rw-r--r--ZArith_dec.v5537logplain
-rw-r--r--ZOdiv.v29342logplain
-rw-r--r--ZOdiv_def.v4833logplain
-rw-r--r--ZOrderedType.v1934logplain
-rw-r--r--Zabs.v6558logplain
-rw-r--r--Zbool.v6848logplain
-rw-r--r--Zcompare.v18886logplain
-rw-r--r--Zcomplements.v6107logplain
-rw-r--r--Zdigits.v9178logplain
-rw-r--r--Zdiv.v34484logplain
-rw-r--r--Zeven.v9840logplain
-rw-r--r--Zgcd_alt.v9749logplain
-rw-r--r--Zhints.v14133logplain
-rw-r--r--Zlogarithm.v7971logplain
-rw-r--r--Zmax.v3456logplain
-rw-r--r--Zmin.v3046logplain
-rw-r--r--Zminmax.v5956logplain
-rw-r--r--Zmisc.v3130logplain
-rw-r--r--Znat.v8371logplain
-rw-r--r--Znumtheory.v41604logplain
-rw-r--r--Zorder.v30194logplain
-rw-r--r--Zpow_def.v790logplain
-rw-r--r--Zpow_facts.v15119logplain
-rw-r--r--Zpower.v12023logplain
-rw-r--r--Zsqrt.v7267logplain
-rw-r--r--Zwf.v2700logplain
-rw-r--r--auxiliary.v3579logplain
-rwxr-xr-xintro.tex238logplain
-rw-r--r--vo.itarget344logplain