From 57ef3e2c400d0be06b7a9a2c5f07e5f34240fe64 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 18 Nov 2010 14:40:10 +0000
Subject: NZSqrt: we define sqrt_up, a square root that rounds up instead of
 down as sqrt

   Some more results about sqrt. Similar results for sqrt_up.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13649 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/Abstract/ZProperties.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 9a592e8ac2..d04443d9ca 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -13,6 +13,6 @@ Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor
 
 Module Type ZProp (Z:ZAxiomsSig) :=
  ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
- <+ NZSqrtProp Z Z
+ <+ NZSqrtProp Z Z <+ NZSqrtUpProp Z Z
  <+ NZLog2Prop Z Z Z <+ NZLog2UpProp Z Z Z
  <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z.
-- 
cgit v1.2.3