From b81505660118503dc37eacff2939cc6f49c3dcba Mon Sep 17 00:00:00 2001 From: filliatr Date: Tue, 7 May 2002 13:28:32 +0000 Subject: lemmes plus_O_n et plus_Sn_m (pour Yves) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2672 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/Peano.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index a025d148b..83f3dda1e 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -88,23 +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