diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-07 13:28:32 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-07 13:28:32 +0000 |
commit | b81505660118503dc37eacff2939cc6f49c3dcba (patch) | |
tree | 03a04a67102b559eeaff249a0624d6926a1865ab /theories/Init/Peano.v | |
parent | d85c5b3a639da751422e6cd342c075941bd6b43f (diff) |
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
Diffstat (limited to 'theories/Init/Peano.v')
-rwxr-xr-x | theories/Init/Peano.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 *) |