diff options
| -rwxr-xr-x | theories/Init/Peano.v | 14 |
1 files 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 *) |