From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Nov 2003 17:28:49 +0000
Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et
 states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Compare.v | 43 +++++++++++++++++++++----------------------
 1 file changed, 21 insertions(+), 22 deletions(-)

(limited to 'theories/Arith/Compare.v')

diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 88055f11e9..b5afebd94a 100755
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -9,7 +9,6 @@
 (*i $Id$ i*)
 
 (** Equality is decidable on [nat] *)
-V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
 (*
@@ -19,42 +18,42 @@ Hints Immediate not_eq_sym : arith.
 *)
 Notation not_eq_sym := sym_not_eq.
 
-Implicit Variables Type m,n,p,q:nat.
+Implicit Types m n p q : nat.
 
-Require Arith.
-Require Peano_dec.
-Require Compare_dec.
+Require Import Arith.
+Require Import Peano_dec.
+Require Import Compare_dec.
 
 Definition le_or_le_S := le_le_S_dec.
 
-Definition compare := gt_eq_gt_dec.
+Definition Pcompare := gt_eq_gt_dec.
 
-Lemma le_dec : (n,m:nat) {le n m} + {le m n}.
+Lemma le_dec : forall n m, {n <= m} + {m <= n}.
 Proof le_ge_dec.
 
-Definition lt_or_eq := [n,m:nat]{(gt m n)}+{n=m}.
+Definition lt_or_eq n m := {m > n} + {n = m}.
 
-Lemma le_decide : (n,m:nat)(le n m)->(lt_or_eq n m).
+Lemma le_decide : forall n m, n <= m -> lt_or_eq n m.
 Proof le_lt_eq_dec.
 
-Lemma le_le_S_eq : (p,q:nat)(le p q)->((le (S p) q)\/(p=q)).
+Lemma le_le_S_eq : forall n m, n <= m -> S n <= m \/ n = m.
 Proof le_lt_or_eq.
 
 (* By special request of G. Kahn - Used in Group Theory *)
-Lemma discrete_nat : (m, n: nat) (lt m n) ->
-   (S m) = n \/ (EX r: nat | n = (S (S (plus m r)))).
+Lemma discrete_nat :
+ 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.
-NewInduction 1; Auto with arith.
-Right; Exists (minus n (S (S m))); Simpl.
-Rewrite (plus_sym m (minus n (S (S m)))).
-Rewrite (plus_n_Sm (minus n (S (S m))) m).
-Rewrite (plus_n_Sm (minus n (S (S m))) (S m)).
-Rewrite (plus_sym (minus 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.
 
-Require Export Min.
+Require Export Min.
\ No newline at end of file
-- 
cgit v1.2.3