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

1 files changed, 7 insertions, 45 deletions

diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index e5c6824193..80d434bab6 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.