From 8907c227f5c456f14617890946aa808ef522d7da Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 9 Sep 2009 16:10:59 +0000
Subject: Znumtheory + Zdiv enriched with stuff from ZMicromega, misc
 improvements

 Mostly results about Zgcd (commutativity, associativity, ...).
 Slight improvement of ZMicromega.

 Beware: some lemmas of Zdiv/ Znumtheory were asking for
 too strict or useless hypothesis. Some minor glitches may occur.

 By the way, some iff lemmas about negb in Bool.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Cyclic/ZModulo/ZModulo.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'theories/Numbers/Cyclic/ZModulo')

diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index b439462db3..7373acc9ad 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -546,7 +546,6 @@ Section ZModulo.
   apply Z_div_pos; auto with zarith.
   subst a; auto with zarith.
   apply Zdiv_lt_upper_bound; auto with zarith.
-  subst a; auto with zarith.
   subst a.
   replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring.
   apply Zlt_le_trans with ([|a1|]*wB+wB); auto with zarith.
-- 
cgit v1.2.3