summaryrefslogtreecommitdiff
path: root/theories/ZArith
ModeNameSize
-rw-r--r--BinInt.v33512logplain
-rw-r--r--Int.v13495logplain
-rw-r--r--Wf_Z.v8204logplain
-rw-r--r--ZArith.v825logplain
-rw-r--r--ZArith_base.v1281logplain
-rw-r--r--ZArith_dec.v5486logplain
-rw-r--r--ZOdiv.v29342logplain
-rw-r--r--ZOdiv_def.v4833logplain
-rw-r--r--ZOrderedType.v1934logplain
-rw-r--r--Zabs.v6513logplain
-rw-r--r--Zbool.v6802logplain
-rw-r--r--Zcompare.v18886logplain
-rw-r--r--Zcomplements.v6054logplain
-rw-r--r--Zdigits.v9130logplain
-rw-r--r--Zdiv.v34439logplain
-rw-r--r--Zeven.v9794logplain
-rw-r--r--Zgcd_alt.v9700logplain
-rw-r--r--Zhints.v14086logplain
-rw-r--r--Zlogarithm.v7920logplain
-rw-r--r--Zmax.v3411logplain
-rw-r--r--Zmin.v3001logplain
-rw-r--r--Zminmax.v5956logplain
-rw-r--r--Zmisc.v3084logplain
-rw-r--r--Znat.v8326logplain
-rw-r--r--Znumtheory.v41553logplain
-rw-r--r--Zorder.v30147logplain
-rw-r--r--Zpow_def.v790logplain
-rw-r--r--Zpow_facts.v15068logplain
-rw-r--r--Zpower.v11976logplain
-rw-r--r--Zsqrt.v7221logplain
-rw-r--r--Zwf.v2656logplain
-rw-r--r--auxiliary.v3529logplain
-rwxr-xr-xintro.tex238logplain
-rw-r--r--vo.itarget344logplain