From 8be0a95911d2d042e5aff31373b9812cc299db87 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter
Date: Fri, 10 Aug 2018 16:54:10 -0400
Subject: one more fix to formulation of the Euclid Theorem in comment

as pointed out by @jashug
---
 theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 63f17341af..5a7bd9ab30 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -13,7 +13,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
 (** * Euclidean Division for integers, Euclid convention
 
     We use here the "usual" formulation of the Euclid Theorem
-    [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 < r < |b| ]
+    [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b| ]
 
     The outcome of the modulo function is hence always positive.
     This corresponds to convention "E" in the following paper:
-- 
cgit v1.2.3