4 files changed, 82 insertions, 2 deletions
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index ece3475dc3..93121d48f2 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -13,7 +13,7 @@ Require Export ZArith_base.
 (** Extra modules using [Omega] or [Ring]. *)
 
 Require Export Zcomplements.
-Require Export Zsqrt.
+Require Export Zsqrt_def.
 Require Export Zpower.
 Require Export Zdiv.
 Require Export Zlogarithm.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt_compat.v
index 20fa6bb5a4..ce46aa6d4f 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -11,6 +11,16 @@ Require Import Omega.
 Require Export ZArith_base.
 Open Local Scope Z_scope.
 
+(**    !! This file is deprecated !!
+
+    Please use rather Zsqrt_def.Zsqrt (or Zsqrtrem).
+    Unlike here, proofs there are fully separated from functions.
+    Some equivalence proofs between the old and the new versions
+    can be found below. A Require Import ZArith provides by default
+    the new versions.
+
+*)
+
 (**********************************************************************)
 (** Definition and properties of square root on Z *)
 
@@ -211,3 +221,12 @@ Proof.
 Qed.
 
 
+(** Equivalence between Zsqrt_plain and [Zsqrt_def.Zsqrt] *)
+
+Lemma Zsqrt_equiv : forall n, Zsqrt_plain n = Zsqrt_def.Zsqrt n.
+Proof.
+ intros. destruct (Z_le_gt_dec 0 n).
+ symmetry. apply Z.sqrt_unique; trivial.
+ now apply Zsqrt_interval.
+ now destruct n.
+Qed.
+\ No newline at end of file
diff --git a/theories/ZArith/Zsqrt_def.v b/theories/ZArith/Zsqrt_def.v
new file mode 100644
index 0000000000..15f4e52751
--- /dev/null
+++ b/theories/ZArith/Zsqrt_def.v
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Definition of a square root function for Z. *)
+
+Require Import BinPos BinInt Psqrt.
+
+Open Scope Z_scope.
+
+Definition Zsqrtrem n :=
+ match n with
+  | 0 => (0, 0)
+  | Zpos p =>
+    match Psqrtrem p with
+     | (s, IsPos r) => (Zpos s, Zpos r)
+     | (s, _) => (Zpos s, 0)
+    end
+  | Zneg _ => (0,0)
+ end.
+
+Definition Zsqrt n :=
+ match n with
+  | 0 => 0
+  | Zpos p => Zpos (Psqrt p)
+  | Zneg _ => 0
+ end.
+
+Lemma Zsqrtrem_spec : forall n, 0<=n ->
+ let (s,r) := Zsqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
+Proof.
+ destruct n. now repeat split.
+ generalize (Psqrtrem_spec p). simpl.
+ destruct 1; simpl; subst; now repeat split.
+ now destruct 1.
+Qed.
+
+Lemma Zsqrt_spec : forall n, 0<=n ->
+ let s := Zsqrt n in s*s <= n < (Zsucc s)*(Zsucc s).
+Proof.
+ destruct n. now repeat split. unfold Zsqrt.
+ rewrite <- Zpos_succ_morphism. intros _. apply (Psqrt_spec p).
+ now destruct 1.
+Qed.
+
+Lemma Zsqrt_neg : forall n, n<0 -> Zsqrt n = 0.
+Proof.
+ intros. now destruct n.
+Qed.
+
+Lemma Zsqrtrem_sqrt : forall n, fst (Zsqrtrem n) = Zsqrt n.
+Proof.
+ destruct n; try reflexivity.
+ unfold Zsqrtrem, Zsqrt, Psqrt.
+ destruct (Psqrtrem p) as (s,r). now destruct r.
+Qed.
+\ No newline at end of file
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 59994e32fd..28db6848dc 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -27,5 +27,6 @@ Zorder.vo
 Zpow_def.vo
 Zpower.vo
 Zpow_facts.vo
-Zsqrt.vo
+Zsqrt_compat.vo
 Zwf.vo
+Zsqrt_def.vo