diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 16:00:43 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 16:00:43 +0000 |
| commit | d857c99c6c985eb36ce8a4b2667dc0b5ccca115c (patch) | |
| tree | 2ea53c80dd3319b24c38b15cb5be5a582c9b302a /theories/Arith/Plus.v | |
| parent | 4837b599b4f158decc91f615a25e3a636c6ced5d (diff) | |
Library doc adjustments (until page 140)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Plus.v')
| -rwxr-xr-x | theories/Arith/Plus.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 67121590e..1b70e1512 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -22,8 +22,7 @@ Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith. Qed. Hints Immediate plus_sym : arith v62. -Lemma plus_Snm_nSm : - (n,m:nat)(plus (S n) m)=(plus n (S m)). +Lemma plus_Snm_nSm : (n,m:nat)(plus (S n) m)=(plus n (S m)). Intros. Simpl. Rewrite -> (plus_sym n m). @@ -143,7 +142,8 @@ Proof. Intros. Discriminate H. Qed. -Lemma plus_is_one : (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}. +Lemma plus_is_one : + (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}. Proof. Destruct m; Auto. Destruct n; Auto. |