diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-09 07:59:19 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-09 07:59:19 +0000 |
| commit | df9a4f1ae642cbbd2a6f1a3b82ad8169b7ec5ae6 (patch) | |
| tree | 47f00369a7e6ceef22bdd4ab7406091b58108924 /theories/Arith/Plus.v | |
| parent | c04fe01b5d33b5e091c8fd19047514a7e4c4f311 (diff) | |
Making the sumbool functions transparent, so that they can used to
compute even inside Coq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2846 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Plus.v')
| -rwxr-xr-x | theories/Arith/Plus.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 0cd20e094..5263cb375 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -140,14 +140,14 @@ Proof. Intros. Discriminate H. Qed. -Lemma plus_is_one : +Definition plus_is_one : (m,n:nat) (m+n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}. Proof. NewDestruct m; Auto. NewDestruct n; Auto. Intros. Simpl in H. Discriminate H. -Qed. +Defined. Lemma plus_permute_2_in_4 : (a,b,c,d:nat) ((a+b)+(c+d))=((a+c)+(b+d)). Proof. |