Arith's min and max placed in Peano (+basic specs max_l and co)

This allow for instance to remove the dependency of List.v toward Min.v
To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano.

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

3 files changed, 4 insertions, 7 deletions

diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index d85178dea..6140eeb5a 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -84,8 +84,7 @@ Hint Immediate le_Sn_le: arith v62.
 
 Theorem le_S_n : forall n m, S n <= S m -> n <= m.
 Proof.
-  intros n m H; change (pred (S n) <= pred (S m)) in |- *.
-  destruct H; simpl; auto with arith.
+  exact Peano.le_S_n.
 Qed.
 Hint Immediate le_S_n: arith v62.
 
@@ -105,11 +104,9 @@ Hint Resolve le_pred_n: arith v62.
 
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
-  destruct n; simpl; auto with arith.
-  destruct m; simpl; auto with arith.
+  exact Peano.le_pred.
 Qed.
 
-
 (** * [le] is a order on [nat] *)
 (** Antisymmetry *)
 
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 592cf489e..b94cc2485 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -15,7 +15,7 @@ Require Export NPeano.
 Local Open Scope nat_scope.
 Implicit Types m n p : nat.
 
-Notation max := max (only parsing).
+Notation max := Peano.max (only parsing).
 
 Definition max_0_l := Nat.max_0_l.
 Definition max_0_r := Nat.max_0_r.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 788fa6a28..ba03a40bd 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -15,7 +15,7 @@ Require Export NPeano.
 Open Local Scope nat_scope.
 Implicit Types m n p : nat.
 
-Notation min := min (only parsing).
+Notation min := Peano.min (only parsing).
 
 Definition min_0_l := Nat.min_0_l.
 Definition min_0_r := Nat.min_0_r.