(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                 ZArith.v                                 *)
(****************************************************************************)

Require Export fast_integer.
Require Export zarith_aux.
Require Export auxiliary.
Require Export Zsyntax.
Require Export ZArith_dec.
Require Export Zmisc.
Require Export Wf_Z.

Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
