5 files changed, 34 insertions, 15 deletions

diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index 92e90b9c8..4a9cf536b 100644
--- a/theories/Numbers/Natural/Abstract/NSqrt.v
+++ b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -22,17 +22,17 @@ Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A).
 Lemma sqrt_spec' : forall a, √a*√a <= a < S (√a) * S (√a).
 Proof. wrap sqrt_spec. Qed.
 
-Lemma sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b.
-Proof. wrap sqrt_unique. Qed.
+Definition sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b
+ := sqrt_unique.
 
 Lemma sqrt_square : forall a, √(a*a) == a.
 Proof. wrap sqrt_square. Qed.
 
-Lemma sqrt_le_mono : forall a b, a<=b -> √a <= √b.
-Proof. wrap sqrt_le_mono. Qed.
+Definition sqrt_le_mono : forall a b, a<=b -> √a <= √b
+ := sqrt_le_mono.
 
-Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.
-Proof. wrap sqrt_lt_cancel. Qed.
+Definition sqrt_lt_cancel : forall a b, √a < √b -> a < b
+ := sqrt_lt_cancel.
 
 Lemma sqrt_le_square : forall a b, b*b<=a <-> b <= √a.
 Proof. wrap sqrt_le_square. Qed.
@@ -44,19 +44,20 @@ Definition sqrt_0 := sqrt_0.
 Definition sqrt_1 := sqrt_1.
 Definition sqrt_2 := sqrt_2.
 
-Definition sqrt_lt_lin : forall a, 1<a -> √a<a := sqrt_lt_lin.
+Definition sqrt_lt_lin : forall a, 1<a -> √a<a
+ := sqrt_lt_lin.
 
-Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.
+Lemma sqrt_le_lin : forall a, √a<=a.
 Proof. wrap sqrt_le_lin. Qed.
 
-Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
-Proof. wrap sqrt_mul_below. Qed.
+Definition sqrt_mul_below : forall a b, √a * √b <= √(a*b)
+ := sqrt_mul_below.
 
 Lemma sqrt_mul_above : forall a b, √(a*b) < S (√a) * S (√b).
 Proof. wrap sqrt_mul_above. Qed.
 
-Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.
-Proof. wrap sqrt_add_le. Qed.
+Definition sqrt_add_le : forall a b, √(a+b) <= √a + √b
+ := sqrt_add_le.
 
 Lemma add_sqrt_le : forall a b, √a + √b <= √(2*(a+b)).
 Proof. wrap add_sqrt_le. Qed.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index ec0fa89bf..60a836d41 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -746,7 +746,7 @@ Module Make (W0:CyclicType) <: NType.
  Theorem spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
  Proof.
   intros x.
-  symmetry. apply Z.sqrt_unique. apply spec_pos.
+  symmetry. apply Z.sqrt_unique.
   rewrite <- ! Zpower_2. apply spec_sqrt_aux.
  Qed.
 
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 348eee5ed..8b7b06966 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -163,14 +163,18 @@ Definition odd_spec := Nodd_spec.
 
 (** Power *)
 
+Program Instance pow_wd : Proper (eq==>eq==>eq) Npow.
 Definition pow_0_r := Npow_0_r.
 Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p.
-Program Instance pow_wd : Proper (eq==>eq==>eq) Npow.
+Lemma pow_neg_r : forall a b, b<0 -> a^b = 0.
+Proof. destruct b; discriminate. Qed.
 
 (** Sqrt *)
 
 Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt.
 Definition sqrt_spec n (H:0<=n) := Nsqrt_spec n.
+Lemma sqrt_neg : forall a, a<0 -> Nsqrt a = 0.
+Proof. destruct a; discriminate. Qed.
 
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index b91b43e31..de5ef4787 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -369,10 +369,12 @@ Definition odd_spec := odd_spec.
 Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
 Definition pow_0_r := pow_0_r.
 Definition pow_succ_r := pow_succ_r.
+Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed.
 Definition pow := pow.
 
-Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
 Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
+Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
+Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed.
 Definition sqrt := sqrt.
 
 Definition div := div.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index f072fc24a..f242951e5 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -204,6 +204,12 @@ Proof.
  simpl. unfold Zpower_pos; simpl. ring.
 Qed.
 
+Lemma pow_neg_r : forall a b, b<0 -> a^b == 0.
+Proof.
+ intros a b. zify. intro Hb. exfalso.
+ generalize (spec_pos b); omega.
+Qed.
+
 Lemma pow_pow_N : forall a b, a^b == pow_N a (to_N b).
 Proof.
  intros. zify. f_equal.
@@ -230,6 +236,12 @@ Proof.
  intros n. zify. apply Zsqrt_spec.
 Qed.
 
+Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0.
+Proof.
+ intros n. zify. intro H. exfalso.
+ generalize (spec_pos n); omega.
+Qed.
+
 (** Even / Odd *)
 
 Definition Even n := exists m, n == 2*m.