(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*                               Oct 1st 1996                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 ZArith.v                                 *)
(****************************************************************************)

Les fichiers fast_integer, zarith, auxiliary
============================================
Ils sont dus a Pierre Cregut, du CNET de Lannion.
  Dans fast_integer sont definis les entiers signes de base 2 (type Z), ainsi
que les operations de base. 
  Dans zarith, les inegalites sont definies et de nombreux lemmes
d'arithmetique sont prouves.
  Dans auxiliary, on trouve notamment les outils pour injecter une expression
entiere (formee avec plus, mult, le, lt) dans Z. On trouve aussi d'autres
lemmes d'arithmetique.

Le fichier Zsyntax 
==================
Il contient des regles de grammaires pour les expressions arithmetiques. 
On peut rentrer en syntaxe "naturelle" des expressions
baties avec les symboles + - * < <= > >= ~= ?= , des variables et des 
applications de fonctions. Il faut simplement mettre entre parentheses
les expressions, avec un % juste derriere la parenthese ouvrante. Exemples :

	(% 2*x + 2 = 2*(x + 1))
	(% (f (x+y)) = 2 * (f x) * (f y))
	(% n <= n*n < n*n + 1)

Les priorites entre + - et * sont respectees.
Le symbole ~= est la negation de l'egalite. On a aussi ?= qui est 
le symbole infixe du predicat Zcompare. x ?= y vaut EGAL, SUPERIEUR 
ou INFERIEUR selon que x=y, x>y ou x<y.

Bugs
====

* Sur le moins unaire : une expression comme (% 3-4) provoque une erreur
de syntaxe : le lexeur produit (INT "3") et (INT "-4") et la grammaire
ne sait qu'en faire. On contourne le pb en mettant un espace entre le
signe - et le nombre : (% 3 - 4).
Pour des expressions comme (% x-y) ou (%34-x+5) pas de pb.
