6 files changed, 62 insertions, 53 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.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 12a8f7a4b..8779f2b45 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -201,6 +201,16 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 
+Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
+Proof.
+induction 1; auto. destruct m; simpl; auto.
+Qed.
+
+Theorem le_S_n : forall n m, S n <= S m -> n <= m.
+Proof.
+intros n m. exact (le_pred (S n) (S m)).
+Qed.
+
 (** Case analysis *)
 
 Theorem nat_case :
@@ -220,3 +230,43 @@ Proof.
   induction n; auto.
   destruct m as [| n0]; auto.
 Qed.
+
+(** Maximum and minimum : definitions and specifications *)
+
+Fixpoint max n m : nat :=
+  match n, m with
+    | O, _ => m
+    | S n', O => n
+    | S n', S m' => S (max n' m')
+  end.
+
+Fixpoint min n m : nat :=
+  match n, m with
+    | O, _ => 0
+    | S n', O => 0
+    | S n', S m' => S (min n' m')
+  end.
+
+Theorem max_l : forall n m : nat, m <= n -> max n m = n.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.
+
+Theorem max_r : forall n m : nat, n <= m -> max n m = m.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.
+
+Theorem min_l : forall n m : nat, n <= m -> min n m = n.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.
+
+Theorem min_r : forall n m : nat, m <= n -> min n m = m.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 2c89af4f1..b3e37685b 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Le Gt Minus Min Bool.
+Require Import Le Gt Minus Bool.
 
 Set Implicit Arguments.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index e5c682419..80d434bab 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -12,21 +12,7 @@
 
 Require Import Peano Peano_dec Compare_dec EqNat NAxioms NProperties NDiv.
 
-(** Some functions not already encountered: min max div mod *)
-
-Fixpoint max n m : nat :=
-  match n, m with
-    | O, _ => m
-    | S n', O => n
-    | S n', S m' => S (max n' m')
-  end.
-
-Fixpoint min n m : nat :=
-  match n, m with
-    | O, _ => 0
-    | S n', O => 0
-    | S n', S m' => S (min n' m')
-  end.
+(** Functions not already defined: div mod *)
 
 Definition divF div x y := if leb y x then S (div (x-y) y) else 0.
 Definition modF mod x y := if leb y x then mod (x-y) y else x.
@@ -112,12 +98,7 @@ Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
 
 Theorem lt_succ_r : forall n m : nat, n < S m <-> n <= m.
 Proof.
-unfold lt.
-split; [|induction 1; auto].
-assert (le_pred : forall n m, n <= m -> pred n <= pred m).
- induction 1 as [|m' H IH]; auto.
- destruct m'. inversion H; subst; auto. simpl; auto.
-exact (le_pred (S n) (S m)).
+unfold lt; split. apply le_S_n. induction 1; auto.
 Qed.
 
 
@@ -133,30 +114,6 @@ Proof.
 induction n. intro H; inversion H. rewrite lt_succ_r; auto.
 Qed.
 
-Theorem min_l : forall n m : nat, n <= m -> min n m = n.
-Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-rewrite (lt_succ_r n m). auto.
-Qed.
-
-Theorem min_r : forall n m : nat, m <= n -> min n m = m.
-Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-rewrite (lt_succ_r m n). auto.
-Qed.
-
-Theorem max_l : forall n m : nat, m <= n -> max n m = n.
-Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-rewrite (lt_succ_r m n). auto.
-Qed.
-
-Theorem max_r : forall n m : nat, n <= m -> max n m = m.
-Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-rewrite (lt_succ_r n m). auto.
-Qed.
-
 (** Facts specific to natural numbers, not integers. *)
 
 Theorem pred_0 : pred 0 = 0.
@@ -204,8 +161,13 @@ Definition sub := minus.
 Definition mul := mult.
 Definition lt := lt.
 Definition le := le.
+
 Definition min := min.
 Definition max := max.
+Definition max_l := max_l.
+Definition max_r := max_r.
+Definition min_l := min_l.
+Definition min_r := min_r.
 
 Definition eqb_eq := beq_nat_true_iff.
 Definition compare_spec := nat_compare_spec.