From ce0730a894791ea19a2ac372a63c94a141102cf8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 12 Nov 2003 19:20:11 +0000
Subject: Cosmetique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4878 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Le.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 71b020e6ab..c80689836e 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -14,6 +14,13 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
+(** Reflexivity *)
+
+Theorem le_refl : (n:nat)(le n n).
+Proof.
+Exact le_n.
+Qed.
+
 (** Transitivity *)
 
 Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p).
@@ -60,7 +67,7 @@ Elim H ; Simpl ; Auto with arith.
 Qed.
 Hints Immediate le_S_n : arith v62.
 
-Lemma le_pred : (n,m:nat)(le n m)->(le (pred n) (pred m)).
+Theorem le_pred : (n,m:nat)(le n m)->(le (pred n) (pred m)).
 Proof.
 NewInduction n as [|n IHn]. Simpl. Auto with arith.
 NewDestruct m as [|m]. Simpl. Intro H. Inversion H.
-- 
cgit v1.2.3