An update on theories/Numbers.

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

3 files changed, 15 insertions, 13 deletions

diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index fa0bd21a35..0a89132ea6 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -8,6 +8,7 @@ Parameter Inline NZ0 : NZ.
 Parameter Inline NZsucc : NZ -> NZ.
 Parameter Inline NZpred : NZ -> NZ.
 Parameter Inline NZplus : NZ -> NZ -> NZ.
+Parameter Inline NZminus : NZ -> NZ -> NZ.
 Parameter Inline NZtimes : NZ -> NZ -> NZ.
 
 Axiom NZE_equiv : equiv NZ NZE.
@@ -20,6 +21,7 @@ as NZE_rel.
 Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
 Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
 Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
+Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
 Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
 
 Delimit Scope NatIntScope with NatInt.
@@ -31,6 +33,7 @@ Notation "'S'" := NZsucc : NatIntScope.
 Notation "'P'" := NZpred : NatIntScope.
 Notation "1" := (S 0) : NatIntScope.
 Notation "x + y" := (NZplus x y) : NatIntScope.
+Notation "x - y" := (NZminus x y) : NatIntScope.
 Notation "x * y" := (NZtimes x y) : NatIntScope.
 
 Axiom NZpred_succ : forall n : NZ, P (S n) == n.
@@ -42,6 +45,9 @@ Axiom NZinduction :
 Axiom NZplus_0_l : forall n : NZ, 0 + n == n.
 Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
 
+Axiom NZminus_0_r : forall n : NZ, n - 0 == n.
+Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m).
+
 Axiom NZtimes_0_r : forall n : NZ, n * 0 == 0.
 Axiom NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
 
@@ -59,6 +65,8 @@ Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
 
 Notation "x < y" := (NZlt x y) : NatIntScope.
 Notation "x <= y" := (NZle x y) : NatIntScope.
+Notation "x > y" := (NZlt y x) (only parsing) : NatIntScope.
+Notation "x >= y" := (NZle y x) (only parsing) : NatIntScope.
 
 Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
 Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 64cf684896..fbccf049c0 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -69,8 +69,8 @@ End CentralInduction.
 Tactic Notation "NZinduct" ident(n) :=
   induction_maker n ltac:(apply NZinduction).
 
-Tactic Notation "NZinduct" ident(n) constr(z) :=
-  induction_maker n ltac:(apply NZcentral_induction with (z := z)).
+Tactic Notation "NZinduct" ident(n) constr(u) :=
+  induction_maker n ltac:(apply NZcentral_induction with (z := u)).
 
 End NZBasePropFunct.
 
diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v
index d333274ba6..061ab84bbc 100644
--- a/theories/Numbers/NatInt/NZPlus.v
+++ b/theories/Numbers/NatInt/NZPlus.v
@@ -5,17 +5,6 @@ Module NZPlusPropFunct (Import NZAxiomsMod : NZAxiomsSig).
 Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
-(** If H1 : t1 == u1 and H2 : t2 == u2 then "add_equations H1 H2 as H3"
-adds the hypothesis H3 : t1 + t2 == u1 + u2 *)
-Tactic Notation "add_equations" constr(H1) constr(H2) "as" ident(H3) :=
-match (type of H1) with
-| ?t1 == ?u1 => match (type of H2) with
-              | ?t2 == ?u2 => assert (H3 : t1 + t2 == u1 + u2); [now apply NZplus_wd |]
-              | _ => fail 2 ":" H2 "is not an equation"
-              end
-| _ => fail 1 ":" H1 "is not an equation"
-end.
-
 Theorem NZplus_0_r : forall n : NZ, n + 0 == n.
 Proof.
 NZinduct n. now rewrite NZplus_0_l.
@@ -81,6 +70,11 @@ intros n m p. rewrite (NZplus_comm n p); rewrite (NZplus_comm m p).
 apply NZplus_cancel_l.
 Qed.
 
+Theorem NZminus_1_r : forall n : NZ, n - 1 == P n.
+Proof.
+intro n; rewrite NZminus_succ_r; now rewrite NZminus_0_r.
+Qed.
+
 End NZPlusPropFunct.