From afda8af89cd10a31419da859ff136fd1c4c0fa22 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 5 Sep 2003 13:43:43 +0000
Subject: Zabs_Zsgn

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4307 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/zarith_aux.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 936468fef7..81c87f7c1d 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -77,9 +77,9 @@ Proof.
 Destruct x;Intros;Rewrite Zmult_sym;Auto with arith.
 Qed.
 
-Lemma Zabs_Zsgn: (x:Z)(Zabs x)=(Zmult (Zsgn x) x).
+Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x.
 Proof.
-Destruct x;Intros;Auto with arith.
+Destruct x;Intros; Rewrite Zmult_sym; Auto with arith.
 Qed.
 
 (** From [nat] to [Z] *)
-- 
cgit v1.2.3