blob: 7f2863d6da2eb74367e3834456386c07747069cd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: ZArith_base.v,v 1.1.2.1 2004/07/16 19:31:42 herbelin Exp $ *)
(** 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]. *)
V7only [
Require Export fast_integer.
Require Export zarith_aux.
].
Require Export BinPos.
Require Export BinNat.
Require Export BinInt.
Require Export Zcompare.
Require Export Zorder.
Require Export Zeven.
Require Export Zmin.
Require Export Zabs.
Require Export Znat.
Require Export auxiliary.
Require Export Zsyntax.
Require Export ZArith_dec.
Require Export Zbool.
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.
Require Export Zhints.
|
