From d85c5b3a639da751422e6cd342c075941bd6b43f Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 May 2002 13:25:57 +0000
Subject: lemmes plus_O_n et plus_Sn_m (pour Yves)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2671 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Peano.v | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 53439d6b63..a025d148be 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -88,13 +88,23 @@ Lemma plus_n_O : (n:nat) n=(plus n O).
 Proof.
   Induction n ; Simpl ; Auto.
 Qed.
-Hints Resolve plus_n_O : core v62.
+
+Lemma plus_O_n : (n:nat) (plus O n)=n.
+Proof.
+  Auto.
+Qed.
+Hints Resolve plus_n_O plus_O_n : core v62.
 
 Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
 Proof.
   Intros m n; Elim m; Simpl; Auto.
 Qed.
-Hints Resolve plus_n_Sm : core v62.
+
+Lemma plus_Sn_m : (n,m:nat)(plus (S n) m)=(S (plus n m)).
+Proof.
+  Auto.
+Qed.
+Hints Resolve plus_n_Sm plus_Sn_m : core v62.
 
 (** Multiplication *)
 
-- 
cgit v1.2.3