Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 13 insertions, 17 deletions

diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index b11f0517..06898658 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -6,21 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Compare.v 9302 2006-10-27 21:21:17Z barras $ i*)
 
 (** Equality is decidable on [nat] *)
+
 Open Local Scope nat_scope.
 
-(*
-Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p).
-Proof sym_not_eq.
-Hints Immediate not_eq_sym : arith.
-*)
 Notation not_eq_sym := sym_not_eq.
 
 Implicit Types m n p q : nat.
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import Peano_dec.
 Require Import Compare_dec.
 
@@ -41,17 +37,17 @@ Proof le_lt_or_eq.
 
 (* By special request of G. Kahn - Used in Group Theory *)
 Lemma discrete_nat :
- forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))).
+  forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))).
 Proof.
-intros m n H.
-lapply (lt_le_S m n); auto with arith.
-intro H'; lapply (le_lt_or_eq (S m) n); auto with arith.
-induction 1; auto with arith.
-right; exists (n - S (S m)); simpl in |- *.
-rewrite (plus_comm m (n - S (S m))).
-rewrite (plus_n_Sm (n - S (S m)) m).
-rewrite (plus_n_Sm (n - S (S m)) (S m)).
-rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith.
+  intros m n H.
+  lapply (lt_le_S m n); auto with arith.
+  intro H'; lapply (le_lt_or_eq (S m) n); auto with arith.
+  induction 1; auto with arith.
+  right; exists (n - S (S m)); simpl in |- *.
+  rewrite (plus_comm m (n - S (S m))).
+  rewrite (plus_n_Sm (n - S (S m)) m).
+  rewrite (plus_n_Sm (n - S (S m)) (S m)).
+  rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith.
 Qed.
 
 Require Export Wf_nat.