1 files changed, 11 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 276c5e9c6..4cdf322fd 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -23,7 +23,6 @@ End SqrtNotation.
 Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A.
 
 Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A).
- Declare Instance sqrt_wd : Proper (eq==>eq) sqrt.
  Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a).
  Axiom sqrt_neg : forall a, a<0 -> √a == 0.
 End NZSqrtSpec.
@@ -78,6 +77,17 @@ Proof.
  order.
 Qed.
 
+(** Hence sqrt is a morphism *)
+
+Instance sqrt_wd : Proper (eq==>eq) sqrt.
+Proof.
+ intros x x' Hx.
+ destruct (lt_ge_cases x 0) as [H|H].
+ rewrite 2 sqrt_neg; trivial. reflexivity.
+ now rewrite <- Hx.
+ apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec.
+Qed.
+
 (** An alternate specification *)
 
 Lemma sqrt_spec_alt : forall a, 0<=a -> exists r,