Library Coq.ZArith.ZArith_base

Library for manipulating integers based on binary encoding. These are the basic modules, required by Omega and Ring for instance. The full library is ZArith.





Require Export BinPos.

Require Export BinNat.

Require Export BinInt.

Require Export Zcompare.

Require Export Zorder.

Require Export Zeven.

Require Export Zmin.

Require Export Zmax.

Require Export Zminmax.

Require Export Zabs.

Require Export Znat.

Require Export auxiliary.

Require Export ZArith_dec.

Require Export Zbool.

Require Export Zmisc.

Require Export Wf_Z.




Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l

  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l

  Zmult_plus_distr_r: zarith.




Require Export Zhints.