ajout option , Exc --> option, et lemmes dans les theories

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1914 85f007b7-540e-0410-9357-904b9bb8a0f7

20 files changed, 674 insertions, 51 deletions

diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 9c6cd1f427..275712084f 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -23,6 +23,17 @@ Save.
 
 Hints Resolve sumbool_of_bool : bool.
 
+Lemma bool_eq_rec : (b:bool)(P:bool->Set)
+                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
+Induction b; Auto.
+Save.
+
+Lemma bool_eq_ind : (b:bool)(P:bool->Prop)
+                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
+Induction b; Auto.
+Save.
+
+
 (*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
 
 (* Logic connectives on type sumbool *)
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index ca5e2ef993..0d2e03bf20 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -36,6 +36,10 @@ Inductive identity [A:Set; a:A] : A->Set :=
      refl_identity: (identity A a a).
 Hints Resolve refl_identity : core v62.
 
+(* [option A] is the extension of A with a dummy element None *)
+
+Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A).
+
 (* [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
 (* Syntax defined in Specif.v *)
 Inductive sum [A,B:Set] : Set
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8c3ade1cd8..14f3319305 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -60,6 +60,22 @@ Section Equivalence.
 
   Definition iff := [P,Q:Prop] (and (P->Q) (Q->P)).
 
+
+Theorem iff_refl : (a:Prop) (iff a a).
+  Proof.
+    Split; Auto.
+  Qed.
+
+Theorem iff_trans : (a,b,c:Prop) (iff a b) -> (iff b c) -> (iff a c).
+  Proof.
+    Intros a b c (H1,H2) (H3,H4); Split; Auto.
+  Qed.
+
+Theorem iff_sym : (a,b:Prop) (iff a b) -> (iff b a).
+  Proof.
+    Intros a b (H1,H2); Split; Auto.
+  Qed.
+
 End Equivalence.
 
 (* [(IF P Q R)], or more suggestively [(either P and_then Q or_else R)],
@@ -198,6 +214,8 @@ Qed.
 
 Hints Immediate sym_eq sym_not_eq : core v62.
 
+
+
 Syntactic Definition Ex := ex | 1.
 Syntactic Definition Ex2 := ex2 | 1.
 Syntactic Definition All := all | 1.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 4882ea29ca..e7308f1651 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -149,19 +149,34 @@ Section Choice_lemmas.
 
 End Choice_lemmas.
 
-Section Exceptions.
-
   (* A result of type [(Exc A)] is either a normal value of type [A] or 
-     an [error]. *) 
-
-  Inductive Exc [A:Set] : Set := value : A->(Exc A) 
-                               | error : (Exc A).
+     an [error] :
+     [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)]
+     it is implemented using the option type. *) 
 
-End Exceptions.
+Definition Exc := option.
+Definition value := Some.
+Definition error := None.
 
 Syntactic Definition Error := (error ?).
 Syntactic Definition Value := (value ?).
 
+(*
+Definition exc_rec :
+ (A:Set; P:((Exc A)->Set))
+ ((a:A)(P (Value a)))->(P Error)->(e:(Exc A))(P e)
+ := option_rec.
+
+Definition exc_rect :
+ (A:Set; P:((Exc A)->Type))
+ ((a:A)(P (Value a)))->(P Error)->(e:(Exc A))(P e)
+ := option_rect.
+
+Definition exc_ind :
+ (A:Set; P:((Exc A)->Prop))
+ ((a:A)(P (Value a)))->(P Error)->(e:(Exc A))(P e)
+ := option_ind.
+*)
 
 (*******************************)
 (* Self realizing propositions *)
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 3e845fb889..0a6d05956f 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -416,8 +416,8 @@ Fixpoint nth_error [l:list;n:nat] : (Exc A) :=
 
 Definition nth_default : A -> list -> nat -> A :=
   [default,l,n]Cases (nth_error l n) of
-  | (value x) => x
-  | error => default
+  | (Some x) => x
+  | None => default
   end.
 
 
diff --git a/theories/Num/.depend b/theories/Num/.depend
index 24658d7ca7..e231ff8023 100644
--- a/theories/Num/.depend
+++ b/theories/Num/.depend
@@ -6,16 +6,20 @@ OppProps.vo: OppProps.v
 OppProps.vi: OppProps.v
 OppAxioms.vo: OppAxioms.v
 OppAxioms.vi: OppAxioms.v
+NeqProps.vo: NeqProps.v NeqParams.vo NeqAxioms.vo EqParams.vo EqAxioms.vo
+NeqProps.vi: NeqProps.v NeqParams.vo NeqAxioms.vo EqParams.vo EqAxioms.vo
+NeqParams.vo: NeqParams.v Params.vo
+NeqParams.vi: NeqParams.v Params.vo
 NeqDef.vo: NeqDef.v Params.vo EqParams.vo
 NeqDef.vi: NeqDef.v Params.vo EqParams.vo
+NeqAxioms.vo: NeqAxioms.v EqParams.vo NeqParams.vo
+NeqAxioms.vi: NeqAxioms.v EqParams.vo NeqParams.vo
 NatSyntax.vo: NatSyntax.v
 NatSyntax.vi: NatSyntax.v
-NSyntax.vo: NSyntax.v Params.vo EqParams.vo NeqDef.vo
-NSyntax.vi: NSyntax.v Params.vo EqParams.vo NeqDef.vo
+NSyntax.vo: NSyntax.v Params.vo
+NSyntax.vi: NSyntax.v Params.vo
 LtProps.vo: LtProps.v Axioms.vo AddProps.vo
 LtProps.vi: LtProps.v Axioms.vo AddProps.vo
-LeibnizEq.vo: LeibnizEq.v Params.vo
-LeibnizEq.vi: LeibnizEq.v Params.vo
 LeProps.vo: LeProps.v LtProps.vo LeAxioms.vo
 LeProps.vi: LeProps.v LtProps.vo LeAxioms.vo
 LeAxioms.vo: LeAxioms.v Axioms.vo LtProps.vo
@@ -30,27 +34,29 @@ GeAxioms.vo: GeAxioms.v Axioms.vo LtProps.vo
 GeAxioms.vi: GeAxioms.v Axioms.vo LtProps.vo
 EqParams.vo: EqParams.v Params.vo
 EqParams.vi: EqParams.v Params.vo
-EqAxioms.vo: EqAxioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
-EqAxioms.vi: EqAxioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
+EqAxioms.vo: EqAxioms.v Params.vo EqParams.vo NSyntax.vo
+EqAxioms.vi: EqAxioms.v Params.vo EqParams.vo NSyntax.vo
 DiscrProps.vo: DiscrProps.v DiscrAxioms.vo LtProps.vo
 DiscrProps.vi: DiscrProps.v DiscrAxioms.vo LtProps.vo
 DiscrAxioms.vo: DiscrAxioms.v Params.vo NSyntax.vo
 DiscrAxioms.vi: DiscrAxioms.v Params.vo NSyntax.vo
 Definitions.vo: Definitions.v
 Definitions.vi: Definitions.v
-Axioms.vo: Axioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
-Axioms.vi: Axioms.v Params.vo EqParams.vo NeqDef.vo NSyntax.vo
-AddProps.vo: AddProps.v Axioms.vo
-AddProps.vi: AddProps.v Axioms.vo
+Axioms.vo: Axioms.v Params.vo EqParams.vo NSyntax.vo
+Axioms.vi: Axioms.v Params.vo EqParams.vo NSyntax.vo
+AddProps.vo: AddProps.v Axioms.vo EqAxioms.vo NeqProps.vo
+AddProps.vi: AddProps.v Axioms.vo EqAxioms.vo NeqProps.vo
 SubProps.html: SubProps.v
 Params.html: Params.v
 OppProps.html: OppProps.v
 OppAxioms.html: OppAxioms.v
+NeqProps.html: NeqProps.v NeqParams.html NeqAxioms.html EqParams.html EqAxioms.html
+NeqParams.html: NeqParams.v Params.html
 NeqDef.html: NeqDef.v Params.html EqParams.html
+NeqAxioms.html: NeqAxioms.v EqParams.html NeqParams.html
 NatSyntax.html: NatSyntax.v
-NSyntax.html: NSyntax.v Params.html EqParams.html NeqDef.html
+NSyntax.html: NSyntax.v Params.html
 LtProps.html: LtProps.v Axioms.html AddProps.html
-LeibnizEq.html: LeibnizEq.v Params.html
 LeProps.html: LeProps.v LtProps.html LeAxioms.html
 LeAxioms.html: LeAxioms.v Axioms.html LtProps.html
 GtProps.html: GtProps.v
@@ -58,9 +64,9 @@ GtAxioms.html: GtAxioms.v Axioms.html LeProps.html
 GeProps.html: GeProps.v
 GeAxioms.html: GeAxioms.v Axioms.html LtProps.html
 EqParams.html: EqParams.v Params.html
-EqAxioms.html: EqAxioms.v Params.html EqParams.html NeqDef.html NSyntax.html
+EqAxioms.html: EqAxioms.v Params.html EqParams.html NSyntax.html
 DiscrProps.html: DiscrProps.v DiscrAxioms.html LtProps.html
 DiscrAxioms.html: DiscrAxioms.v Params.html NSyntax.html
 Definitions.html: Definitions.v
-Axioms.html: Axioms.v Params.html EqParams.html NeqDef.html NSyntax.html
-AddProps.html: AddProps.v Axioms.html
+Axioms.html: Axioms.v Params.html EqParams.html NSyntax.html
+AddProps.html: AddProps.v Axioms.html EqAxioms.html NeqProps.html
diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
index 5633921464..f30b616162 100644
--- a/theories/Num/AddProps.v
+++ b/theories/Num/AddProps.v
@@ -11,18 +11,6 @@ Require Export EqAxioms.
 
 (*s This file contains basic properties of addition with respect to equality *)
 
-(*s Properties of inequalities *)
-Lemma neq_sym : (x,y:N)(x<>y)->(y<>x).
-Unfold neq; Auto with num.
-Save.
-
-Hints Resolve neq_sym : num.
-
-Lemma neq_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<>x2)->(y1<>y2).
-Red; EAuto with num.
-Save.
-Hints Resolve neq_eq_compat : num.
-
 (*s Properties of Addition *)
 Lemma add_x_0 : (x:N)(x+zero)=x.
 EAuto 3 with num.
@@ -67,4 +55,3 @@ Save.
 Hints Resolve add_one_x_S : num.
 
 
-
diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v
index 804dc479c7..a8c43b6a28 100644
--- a/theories/Num/Axioms.v
+++ b/theories/Num/Axioms.v
@@ -10,7 +10,6 @@
 (*s Axioms for the basic numerical operations *)
 Require Export Params.
 Require Export EqParams.
-Require Export NeqDef.
 Require Export NSyntax.
 
 (*s Axioms for [eq] *)
diff --git a/theories/Num/EqAxioms.v b/theories/Num/EqAxioms.v
index 1741c3d1f5..957a8edf03 100644
--- a/theories/Num/EqAxioms.v
+++ b/theories/Num/EqAxioms.v
@@ -3,7 +3,6 @@
 (*s Axioms for equality *)
 Require Export Params.
 Require Export EqParams.
-Require Export NeqDef.
 Require Export NSyntax.
 
 (*s Basic Axioms for [eq] *)
diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v
index 441dc21dfd..3f15696737 100644
--- a/theories/Num/EqParams.v
+++ b/theories/Num/EqParams.v
@@ -2,11 +2,11 @@
 
 (*s Equality is introduced as an independant parameter, it could be 
     instantiated with Leibniz equality *)
-Require Params.
+Require Export Params.
 
 Parameter eqN:N->N->Prop.  
 
-(*i Infix 6 "=" eq. i*)
+(*i Infix 6 "=" eqN. i*)
 
 Grammar constr constr1 :=
 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v
index 490fbbb128..ef9e523108 100644
--- a/theories/Num/LtProps.v
+++ b/theories/Num/LtProps.v
@@ -7,6 +7,7 @@
 (***********************************************************************)
 Require Export Axioms.
 Require Export AddProps.
+Require Export NeqProps.
 
 (*s This file contains basic properties of the less than relation *)
 
diff --git a/theories/Num/Make b/theories/Num/Make
index d897d8087b..c7c0595c7f 100644
--- a/theories/Num/Make
+++ b/theories/Num/Make
@@ -1,9 +1,14 @@
 Params.v
 EqParams.v
-NeqDef.v
 NSyntax.v
+
 Axioms.v
 EqAxioms.v
+
+NeqParams.v
+NeqAxioms.v
+NeqDef.v
+NeqProps.v
 AddProps.v
 LtProps.v
 OppProps.v
diff --git a/theories/Num/Makefile b/theories/Num/Makefile
new file mode 100644
index 0000000000..fdbe44bb6d
--- /dev/null
+++ b/theories/Num/Makefile
@@ -0,0 +1,343 @@
+##############################################################################
+##                 The Calculus of Inductive Constructions                  ##
+##                                                                          ##
+##                                Projet Coq                                ##
+##                                                                          ##
+##                     INRIA                        ENS-CNRS                ##
+##              Rocquencourt                        Lyon                    ##
+##                                                                          ##
+##                                  Coq V7                                  ##
+##                                                                          ##
+##                                                                          ##
+##############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -f Make -o Makefile 
+#
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+CAMLP4LIB=`camlp4 -where`
+COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
+  -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
+  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
+  -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
+ZFLAGS=$(OCAMLLIBS) $(COQSRC)
+OPT=
+COQFLAGS=-q $(OPT) $(COQLIBS)
+COQC=$(COQBIN)coqc
+GALLINA=gallina
+COQ2HTML=coq2html
+COQ2LATEX=coq2latex
+CAMLC=ocamlc -c
+CAMLOPTC=ocamlopt -c
+CAMLLINK=ocamlc
+CAMLOPTLINK=ocamlopt
+COQDEP=$(COQBIN)coqdep -c
+COQVO2XML=coq_vo2xml
+
+#########################
+#                       #
+# Libraries definition. #
+#                       #
+#########################
+
+OCAMLLIBS=-I .
+COQLIBS=-I .
+
+###################################
+#                                 #
+# Definition of the "all" target. #
+#                                 #
+###################################
+
+all: Params.vo\
+  EqParams.vo\
+  NSyntax.vo\
+  Axioms.vo\
+  EqAxioms.vo\
+  NeqParams.vo\
+  NeqAxioms.vo\
+  NeqDef.vo\
+  NeqProps.vo\
+  AddProps.vo\
+  LtProps.vo\
+  OppProps.vo\
+  SubProps.vo\
+  LeAxioms.vo\
+  LeProps.vo\
+  GtAxioms.vo\
+  GtProps.vo\
+  GeAxioms.vo\
+  GeProps.vo\
+  DiscrAxioms.vo\
+  DiscrProps.vo\
+  OppAxioms.vo\
+  Leibniz\
+  Nat
+
+spec: Params.vi\
+  EqParams.vi\
+  NSyntax.vi\
+  Axioms.vi\
+  EqAxioms.vi\
+  NeqParams.vi\
+  NeqAxioms.vi\
+  NeqDef.vi\
+  NeqProps.vi\
+  AddProps.vi\
+  LtProps.vi\
+  OppProps.vi\
+  SubProps.vi\
+  LeAxioms.vi\
+  LeProps.vi\
+  GtAxioms.vi\
+  GtProps.vi\
+  GeAxioms.vi\
+  GeProps.vi\
+  DiscrAxioms.vi\
+  DiscrProps.vi\
+  OppAxioms.vi
+
+gallina: Params.g\
+  EqParams.g\
+  NSyntax.g\
+  Axioms.g\
+  EqAxioms.g\
+  NeqParams.g\
+  NeqAxioms.g\
+  NeqDef.g\
+  NeqProps.g\
+  AddProps.g\
+  LtProps.g\
+  OppProps.g\
+  SubProps.g\
+  LeAxioms.g\
+  LeProps.g\
+  GtAxioms.g\
+  GtProps.g\
+  GeAxioms.g\
+  GeProps.g\
+  DiscrAxioms.g\
+  DiscrProps.g\
+  OppAxioms.g
+
+html: Params.html\
+  EqParams.html\
+  NSyntax.html\
+  Axioms.html\
+  EqAxioms.html\
+  NeqParams.html\
+  NeqAxioms.html\
+  NeqDef.html\
+  NeqProps.html\
+  AddProps.html\
+  LtProps.html\
+  OppProps.html\
+  SubProps.html\
+  LeAxioms.html\
+  LeProps.html\
+  GtAxioms.html\
+  GtProps.html\
+  GeAxioms.html\
+  GeProps.html\
+  DiscrAxioms.html\
+  DiscrProps.html\
+  OppAxioms.html
+
+tex: Params.tex\
+  EqParams.tex\
+  NSyntax.tex\
+  Axioms.tex\
+  EqAxioms.tex\
+  NeqParams.tex\
+  NeqAxioms.tex\
+  NeqDef.tex\
+  NeqProps.tex\
+  AddProps.tex\
+  LtProps.tex\
+  OppProps.tex\
+  SubProps.tex\
+  LeAxioms.tex\
+  LeProps.tex\
+  GtAxioms.tex\
+  GtProps.tex\
+  GeAxioms.tex\
+  GeProps.tex\
+  DiscrAxioms.tex\
+  DiscrProps.tex\
+  OppAxioms.tex
+
+gallinatex: Params.g.tex\
+  EqParams.g.tex\
+  NSyntax.g.tex\
+  Axioms.g.tex\
+  EqAxioms.g.tex\
+  NeqParams.g.tex\
+  NeqAxioms.g.tex\
+  NeqDef.g.tex\
+  NeqProps.g.tex\
+  AddProps.g.tex\
+  LtProps.g.tex\
+  OppProps.g.tex\
+  SubProps.g.tex\
+  LeAxioms.g.tex\
+  LeProps.g.tex\
+  GtAxioms.g.tex\
+  GtProps.g.tex\
+  GeAxioms.g.tex\
+  GeProps.g.tex\
+  DiscrAxioms.g.tex\
+  DiscrProps.g.tex\
+  OppAxioms.g.tex
+
+gallinahtml: Params.g.html\
+  EqParams.g.html\
+  NSyntax.g.html\
+  Axioms.g.html\
+  EqAxioms.g.html\
+  NeqParams.g.html\
+  NeqAxioms.g.html\
+  NeqDef.g.html\
+  NeqProps.g.html\
+  AddProps.g.html\
+  LtProps.g.html\
+  OppProps.g.html\
+  SubProps.g.html\
+  LeAxioms.g.html\
+  LeProps.g.html\
+  GtAxioms.g.html\
+  GtProps.g.html\
+  GeAxioms.g.html\
+  GeProps.g.html\
+  DiscrAxioms.g.html\
+  DiscrProps.g.html\
+  OppAxioms.g.html
+
+xml:: .xml_time_stamp
+.xml_time_stamp: Params.vo\
+  EqParams.vo\
+  NSyntax.vo\
+  Axioms.vo\
+  EqAxioms.vo\
+  NeqParams.vo\
+  NeqAxioms.vo\
+  NeqDef.vo\
+  NeqProps.vo\
+  AddProps.vo\
+  LtProps.vo\
+  OppProps.vo\
+  SubProps.vo\
+  LeAxioms.vo\
+  LeProps.vo\
+  GtAxioms.vo\
+  GtProps.vo\
+  GeAxioms.vo\
+  GeProps.vo\
+  DiscrAxioms.vo\
+  DiscrProps.vo\
+  OppAxioms.vo
+	$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
+	touch .xml_time_stamp
+
+###################
+#                 #
+# Subdirectories. #
+#                 #
+###################
+
+Leibniz:
+	cd Leibniz ; $(MAKE) all
+
+Nat:
+	cd Nat ; $(MAKE) all
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+.PHONY: all opt byte archclean clean install depend xml Leibniz Nat
+
+.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
+
+.v.vo:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+.v.vi:
+	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+.v.g:
+	$(GALLINA) $<
+
+.v.html:
+	$(COQ2HTML) $<
+
+.v.tex:
+	$(COQ2LATEX) $< -latex -o $@
+
+.v.g.html:
+	$(GALLINA) -stdout $< | $(COQ2HTML) -f > $@
+
+.v.g.tex:
+	$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@
+
+byte:
+	$(MAKE) all "OPT="
+
+opt:
+	$(MAKE) all "OPT=-opt"
+
+include .depend
+
+depend:
+	rm .depend
+	$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
+	$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
+	(cd Leibniz ; $(MAKE) depend)
+	(cd Nat ; $(MAKE) depend)
+
+xml::
+	(cd Leibniz ; $(MAKE) xml)
+	(cd Nat ; $(MAKE) xml)
+
+install:
+	@if test -z $(TARGETDIR); then echo "You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')"; exit 1; fi
+	cp -f *.vo $(TARGETDIR)
+	(cd Leibniz ; $(MAKE) install)
+	(cd Nat ; $(MAKE) install)
+
+Makefile: Make
+	mv -f Makefile Makefile.bak
+	$(COQBIN)coq_makefile -f Make -o Makefile
+
+clean:
+	rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~
+	(cd Leibniz ; $(MAKE) clean)
+	(cd Nat ; $(MAKE) clean)
+
+archclean:
+	rm -f *.cmx *.o
+	(cd Leibniz ; $(MAKE) archclean)
+	(cd Nat ; $(MAKE) archclean)
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index 443056fd89..364fb944a0 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -30,10 +30,6 @@ Grammar constr lassoc_constr4 :=
       esac.
 
 Syntax constr
-  level 1:
-    equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
- ;
-
   level 4:
     sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
 .
\ No newline at end of file
diff --git a/theories/Num/Nat/.depend b/theories/Num/Nat/.depend
index 8e81ee7c9f..8bfdf1fe5f 100644
--- a/theories/Num/Nat/.depend
+++ b/theories/Num/Nat/.depend
@@ -6,10 +6,10 @@ NSyntax.vo: NSyntax.v
 NSyntax.vi: NSyntax.v
 EqAxioms.vo: EqAxioms.v NSyntax.vo
 EqAxioms.vi: EqAxioms.v NSyntax.vo
-Axioms.vo: Axioms.v Params.vo NSyntax.vo
-Axioms.vi: Axioms.v Params.vo NSyntax.vo
+Axioms.vo: Axioms.v Params.vo EqAxioms.vo NSyntax.vo
+Axioms.vi: Axioms.v Params.vo EqAxioms.vo NSyntax.vo
 Params.html: Params.v
 NeqDef.html: NeqDef.v Params.html
 NSyntax.html: NSyntax.v
 EqAxioms.html: EqAxioms.v NSyntax.html
-Axioms.html: Axioms.v Params.html NSyntax.html
+Axioms.html: Axioms.v Params.html EqAxioms.html NSyntax.html
diff --git a/theories/Num/NeqAxioms.v b/theories/Num/NeqAxioms.v
new file mode 100644
index 0000000000..303d30cf04
--- /dev/null
+++ b/theories/Num/NeqAxioms.v
@@ -0,0 +1,25 @@
+(*i $Id $ i*)
+
+(*s InEquality is introduced as an independant parameter, it could be 
+    instantiated with the negation of equality *)
+
+Require Export EqParams.
+Require Export NeqParams.
+
+Axiom eq_not_neq : (x,y:N)x=y->~(x<>y).
+Hints Immediate eq_not_neq : num.
+
+Axiom neq_sym : (x,y:N)(x<>y)->(y<>x).
+Hints Resolve neq_sym : num.
+
+Axiom neq_not_neq_trans : (x,y,z:N)(x<>y)->~(y<>z)->(x<>z).
+Hints Resolve neq_not_neq_trans : num.
+
+
+
+
+
+
+
+
+
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
index 73375e242f..a9ad0dd0b0 100644
--- a/theories/Num/NeqDef.v
+++ b/theories/Num/NeqDef.v
@@ -1,9 +1,30 @@
+(*i $Id $ i*)
 
-(*s Definition of inequality *)
+(*s DisEquality is defined as the negation of equality *)
 
 Require Params.
 Require EqParams.
-Definition neq [x,y:N] := (eqN x y)->False.
+Require EqAxioms.
 
+Definition neq : N -> N -> Prop := [x,y] ~(x=y).
 Infix 6 "<>" neq.
 
+(* Proofs of axioms *)
+Lemma eq_not_neq : (x,y:N)x=y->~(x<>y).
+Unfold neq; Auto with num.
+Save.
+Hints Immediate eq_not_neq : num.
+
+Lemma neq_sym : (x,y:N)(x<>y)->(y<>x).
+Unfold neq; Auto with num.
+Save.
+Hints Resolve neq_sym : num.
+
+Lemma neq_not_neq_trans : (x,y,z:N)(x<>y)->~(y<>z)->(x<>z).
+Unfold neq; EAuto with num.
+Save.
+Hints Resolve neq_not_neq_trans : num.
+
+
+
+
diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v
new file mode 100644
index 0000000000..0486eb24ad
--- /dev/null
+++ b/theories/Num/NeqParams.v
@@ -0,0 +1,17 @@
+(*i $Id $ i*)
+
+(*s InEquality is introduced as an independant parameter, it could be 
+    instantiated with the negation of equality *)
+
+Require Export Params.
+
+Parameter neq : N -> N -> Prop.
+
+Infix 6 "<>" neq.
+
+
+
+
+
+
+
diff --git a/theories/Num/NeqProps.v b/theories/Num/NeqProps.v
new file mode 100644
index 0000000000..ca521493dd
--- /dev/null
+++ b/theories/Num/NeqProps.v
@@ -0,0 +1,50 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+Require Export NeqParams.
+Require Export NeqAxioms.
+Require Export EqParams.
+Require Export EqAxioms.
+
+
+(*s This file contains basic properties of disequality *)
+
+Lemma neq_antirefl : (x:N)~(x<>x).
+Auto with num.
+Save.
+Hints Resolve neq_antirefl : num.
+
+Lemma eq_not_neq_y_x : (x,y:N)(x=y)->~(y<>x).
+Intros; Apply eq_not_neq; Auto with num.
+Save.
+Hints Immediate eq_not_neq_y_x : num.
+
+Lemma neq_not_eq : (x,y:N)(x<>y)->~(x=y).
+Red; Intros; Apply (eq_not_neq x y); Trivial.
+Save.
+Hints Immediate neq_not_eq : num.
+
+Lemma neq_not_eq_y_x : (x,y:N)(x<>y)->~(y=x).
+Intros; Apply neq_not_eq; Auto with num.
+Save.
+Hints Immediate neq_not_eq_y_x : num.
+
+Lemma not_neq_neq_trans : (x,y,z:N)~(x<>y)->(y<>z)->(x<>z).
+Intros; Apply neq_sym; Apply neq_not_neq_trans with y; Auto with num.
+Save.
+Hints Resolve not_neq_neq_trans : num.
+
+Lemma neq_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<>x2)->(y1<>y2).
+Intros.
+EAuto with num.
+Save.
+
+
+
+
+
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index cf46b8bdfb..425baa53c5 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -83,6 +83,7 @@ Definition Zgt_bool := [x,y:Z]Case ` x ?= y` of false false true end.
 Definition Zeq_bool := [x,y:Z]Cases `x ?= y` of EGAL => true | _ => false end.
 Definition Zneq_bool := [x,y:Z]Cases `x ?= y` of EGAL =>false | _ => true end.
 
+
 End numbers.
 
 Section iterate.
@@ -432,6 +433,131 @@ Compute. Intro H0. Discriminate H0. Intuition.
 Intros. Absurd `0 <= (NEG p)`. Compute. Auto with arith. Intuition.
 Save.
 
+(* Lemmas on Zle_bool used in contrib/graphs *)
+
+Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y).
+Proof.
+  Unfold Zle_bool Zle. Intros x y. Unfold not. Case (Zcompare x y). Intros. Discriminate H0.
+  Intros. Discriminate H0.
+  Intro. Discriminate H.
+Qed.
+
+Lemma Zle_imp_le_bool : (x,y:Z) (Zle x y) -> (Zle_bool x y)=true.
+Proof.
+  Unfold Zle Zle_bool. Intros x y. Case (Zcompare x y); Trivial. Intro. Elim (H (refl_equal ? ?)).
+Qed.
+
+Lemma Zle_bool_refl : (x:Z) (Zle_bool x x)=true.
+Proof.
+  Intro. Apply Zle_imp_le_bool. Apply Zle_refl. Reflexivity.
+Qed.
+
+Lemma Zle_bool_antisym : (x,y:Z) (Zle_bool x y)=true -> (Zle_bool y x)=true -> x=y.
+Proof.
+  Intros. Apply Zle_antisym. Apply Zle_bool_imp_le. Assumption.
+  Apply Zle_bool_imp_le. Assumption.
+Qed.
+
+Lemma Zle_bool_trans : (x,y,z:Z) (Zle_bool x y)=true -> (Zle_bool y z)=true -> (Zle_bool x z)=true.
+Proof.
+  Intros. Apply Zle_imp_le_bool. Apply Zle_trans with m:=y. Apply Zle_bool_imp_le. Assumption.
+  Apply Zle_bool_imp_le. Assumption.
+Qed.
+
+Lemma Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}.
+Proof.
+  Intros. Unfold Zle_bool. Cut (Zcompare x y)=SUPERIEUR<->(Zcompare y x)=INFERIEUR.
+  Case (Zcompare x y). Left . Reflexivity.
+  Left . Reflexivity.
+  Right . Rewrite (proj1 ? ? H (refl_equal ? ?)). Reflexivity.
+  Apply Zcompare_ANTISYM.
+Qed.
+
+Lemma Zle_bool_plus_mono : (x,y,z,t:Z) (Zle_bool x y)=true -> (Zle_bool z t)=true ->
+                                (Zle_bool (Zplus x z) (Zplus y t))=true.
+Proof.
+  Intros. Apply Zle_imp_le_bool. Apply Zle_plus_plus. Apply Zle_bool_imp_le. Assumption.
+  Apply Zle_bool_imp_le. Assumption.
+Qed.
+
+Lemma Zone_pos : (Zle_bool `1` `0`)=false.
+Proof.
+  Reflexivity.
+Qed.
+
+Lemma Zone_min_pos : (x:Z) (Zle_bool x `0`)=false -> (Zle_bool `1` x)=true.
+Proof.
+  Intros. Apply Zle_imp_le_bool. Change (Zle (Zs ZERO) x). Apply Zgt_le_S. Generalize H.
+  Unfold Zle_bool Zgt. Case (Zcompare x ZERO). Intro H0. Discriminate H0.
+  Intro H0. Discriminate H0.
+  Reflexivity.
+Qed.
+
+
+ Lemma Zle_is_le_bool : (x,y:Z) (Zle x y) <-> (Zle_bool x y)=true.
+  Proof.
+    Intros. Split. Intro. Apply Zle_imp_le_bool. Assumption.
+    Intro. Apply Zle_bool_imp_le. Assumption.
+  Qed.
+
+  Lemma Zge_is_le_bool : (x,y:Z) (Zge x y) <-> (Zle_bool y x)=true.
+  Proof.
+    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zge_le. Assumption.
+    Intro. Apply Zle_ge. Apply Zle_bool_imp_le. Assumption.
+  Qed.
+
+  Lemma Zlt_is_le_bool : (x,y:Z) (Zlt x y) <-> (Zle_bool x `y-1`)=true.
+  Proof.
+    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zlt_n_Sm_le. Rewrite (Zs_pred y) in H.
+    Assumption.
+    Intro. Rewrite (Zs_pred y). Apply Zle_lt_n_Sm. Apply Zle_bool_imp_le. Assumption.
+  Qed.
+
+  Lemma Zgt_is_le_bool : (x,y:Z) (Zgt x y) <-> (Zle_bool y `x-1`)=true.
+  Proof.
+    Intros. Apply iff_trans with b:=`y < x`. Split. Exact (Zgt_lt x y).
+    Exact (Zlt_gt y x).
+    Exact (Zlt_is_le_bool y x).
+  Qed.
 
 End arith.
 
+(* Equivalence between inequalities used in contrib/graph *)
+
+
+  Lemma Zle_plus_swap : (x,y,z:Z) `x+z<=y` <-> `x<=y-z`.
+  Proof.
+    Intros. Split. Intro. Rewrite <- (Zero_right x). Rewrite <- (Zplus_inverse_r z).
+    Rewrite Zplus_assoc_l. Exact (Zle_reg_r ? ? ? H).
+    Intro. Rewrite <- (Zero_right y). Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_l.
+    Apply Zle_reg_r. Assumption.
+  Qed.
+
+  Lemma Zge_iff_le : (x,y:Z) `x>=y` <-> `y<=x`.
+  Proof.
+    Intros. Split. Intro. Apply Zge_le. Assumption.
+    Intro. Apply Zle_ge. Assumption.
+  Qed.
+
+  Lemma Zlt_plus_swap : (x,y,z:Z) `x+z<y` <-> `x<y-z`.
+  Proof.
+    Intros. Split. Intro. Unfold Zminus. Rewrite Zplus_sym. Rewrite <- (Zero_left x).
+    Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym.
+    Assumption.
+    Intro. Rewrite Zplus_sym. Rewrite <- (Zero_left y). Rewrite <- (Zplus_inverse_r z).
+    Rewrite Zplus_assoc_r. Apply Zlt_reg_l. Rewrite Zplus_sym. Assumption.
+  Qed.
+
+  Lemma Zgt_iff_lt : (x,y:Z) `x>y` <-> `y<x`.
+  Proof.
+    Intros. Split. Intro. Apply Zgt_lt. Assumption.
+    Intro. Apply Zlt_gt. Assumption.
+  Qed.
+
+  Lemma Zeq_plus_swap : (x,y,z:Z) `x+z=y` <-> `x=y-z`.
+  Proof.
+    Intros. Split. Intro. Rewrite <- H. Unfold Zminus. Rewrite Zplus_assoc_r.
+    Rewrite Zplus_inverse_r. Apply sym_eq. Apply Zero_right.
+    Intro. Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r. Rewrite Zplus_inverse_l.
+    Apply Zero_right.
+  Qed.