Déplacement de minus dans Peano

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

2 files changed, 10 insertions, 0 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 83f3dda1e..a3774efb6 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -127,6 +127,15 @@ Proof.
 Qed.
 Hints Resolve mult_n_Sm : core v62.
 
+(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
+
+Fixpoint minus [n:nat] : nat -> nat := 
+  [m:nat]Cases n m of
+            O    _     =>  O
+         | (S k) O     => (S k)
+         | (S k) (S l) => (minus k l)
+        end. 
+
 (** Definition of the usual orders, the basic properties of [le] and [lt] 
     can be found in files Le and Lt *)
 
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index b223f371f..072be35dd 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -26,6 +26,7 @@ Module nat_scope.
 Open Scope nat_scope.
 
 Infix 4 "+" plus : nat_scope V8only (left associativity).
+Infix 4 "-" minus : nat_scope V8only (left associativity).
 Infix 3 "*" mult : nat_scope V8only (left associativity).
 Infix NONA 5 "<=" le : nat_scope.
 Infix NONA 5 "<" lt : nat_scope.