From 63e792e2cf320544bcd8b28b2e932b18d5f4af1f Mon Sep 17 00:00:00 2001
From: emakarov
Date: Thu, 22 Nov 2007 14:34:44 +0000
Subject: An update on Numbers. Added two files dealing with recursion, for
 information only.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10330 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/Abstract/ZPlus.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Integer/Abstract/ZPlus.v')

diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index b0cebd482d..cbe22077e0 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -38,7 +38,7 @@ Proof Zopp_0.
 Theorem Zopp_succ : forall n : Z, - (S n) == P (- n).
 Proof Zopp_succ.
 
-(** Theorems that are valid for both natural numbers and integers *)
+(* Theorems that are valid for both natural numbers and integers *)
 
 Theorem Zplus_0_r : forall n : Z, n + 0 == n.
 Proof NZplus_0_r.
@@ -70,7 +70,7 @@ Proof NZplus_cancel_l.
 Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
 Proof NZplus_cancel_r.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
 Theorem Zplus_pred_l : forall n m : Z, P n + m == P (n + m).
 Proof.
@@ -200,6 +200,11 @@ intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc.
 now rewrite Zplus_opp_r.
 Qed.
 
+Theorem minus_opp_l : forall n m : Z, - n - m == - m - n.
+Proof.
+intros n m. do 2 rewrite <- Zplus_opp_r. now rewrite Zplus_comm.
+Qed.
+
 Theorem Zminus_opp_r : forall n m : Z, n - (- m) == n + m.
 Proof.
 intros n m; rewrite <- Zplus_opp_r; now rewrite Zopp_involutive.
-- 
cgit v1.2.3