2 files changed, 18 insertions, 4 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index be201f2d66..37f5b294e1 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -78,13 +78,12 @@ Module Type ZType.
  Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, 0 <= [x] ->
-   [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
+ Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
  Parameter spec_div_eucl: forall x y,
    let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b).
+ Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
  Parameter spec_even : forall x, even x = Zeven_bool [x].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 3e63755434..d632d22607 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -18,7 +18,7 @@ Module ZTypeIsZAxioms (Import Z : ZType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
- spec_mul spec_opp spec_of_Z spec_div spec_modulo
+ spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
  spec_pow spec_even spec_odd
  : zsimpl.
@@ -278,6 +278,21 @@ Proof.
  intros a b. red. now rewrite spec_pow_N, spec_pow_pos.
 Qed.
 
+(** Sqrt *)
+
+Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
+
+Lemma sqrt_spec : forall n, 0<=n ->
+ (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)).
+Proof.
+ intros n. zify. apply Zsqrt_spec.
+Qed.
+
+Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0.
+Proof.
+ intros n. zify. apply Zsqrt_neg.
+Qed.
+
 (** Even / Odd *)
 
 Definition Even n := exists m, n == 2*m.