Numbers: specs about sqrt and pow of neg numbers, even in NZ

 These additional specs are useless (but trivially provable) for N.
 They are quite convenient when deriving properties in NZ.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13603 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 126 insertions, 124 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 4f88008be4..6e6cd7f0fc 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -70,26 +70,16 @@ Module Type Parity (Import Z : ZAxiomsMiniSig').
  Axiom odd_spec : forall n, odd n = true <-> Odd n.
 End Parity.
 
-(** For the power function, we just add to NZPow an addition spec *)
-
-Module Type ZPowSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Pow' Z).
- Axiom pow_neg : forall a b, b<0 -> a^b == 0.
-End ZPowSpecNeg.
-
-(** Same for the sqrt function. *)
-
-Module Type ZSqrtSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Sqrt' Z).
- Axiom sqrt_neg : forall a, a<0 -> √a == 0.
-End ZSqrtSpecNeg.
+(** For the power and sqrt functions, the NZ axiomatizations are enough. *)
 
 (** Let's group everything *)
 
 Module Type ZAxiomsSig :=
   ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow <+ ZPowSpecNeg <+ NZSqrt.NZSqrt <+ ZSqrtSpecNeg.
+   <+ NZPow.NZPow <+ NZSqrt.NZSqrt.
 Module Type ZAxiomsSig' :=
   ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow' <+ ZPowSpecNeg <+ NZSqrt.NZSqrt' <+ ZSqrtSpecNeg.
+   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt'.
 
 
 (** Division is left apart, since many different flavours are available *)
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 0241c34762..8ea0122506 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -18,49 +18,6 @@ Module Type ZPowProp
 
  Include NZPowProp A A B.
 
-(** Many results are directly the same as in NZPow, hence
-    the Include above. We extend nonetheless a few of them,
-    and add some results concerning negative first arg.
-*)
-
-Lemma pow_mul_l' : forall a b c, (a*b)^c == a^c * b^c.
-Proof.
- intros a b c. destruct (le_gt_cases 0 c). now apply pow_mul_l.
- rewrite !pow_neg by trivial. now nzsimpl.
-Qed.
-
-Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b.
-Proof.
- intros a b Ha. destruct (le_gt_cases 0 b).
- now apply pow_nonneg_nonneg.
- rewrite !pow_neg by trivial. order.
-Qed.
-
-Lemma pow_le_mono_l' : forall a b c, 0<=a<=b -> a^c <= b^c.
-Proof.
- intros a b c. destruct (le_gt_cases 0 c). now apply pow_le_mono_l.
- rewrite !pow_neg by trivial. order.
-Qed.
-
-(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *)
-
-Lemma pow_le_mono_r' : forall a b c, 0<a -> b<=c -> a^b <= a^c.
-Proof.
- intros a b c. destruct (le_gt_cases 0 b).
- intros. apply pow_le_mono_r; try split; trivial.
- rewrite !pow_neg by trivial.
- intros. apply pow_nonneg. order.
-Qed.
-
-Lemma pow_le_mono' : forall a b c d, 0<a<=c -> b<=d ->
- a^b <= c^d.
-Proof.
- intros a b c d. destruct (le_gt_cases 0 b).
- intros. apply pow_le_mono. trivial. split; trivial.
- rewrite !pow_neg by trivial.
- intros. apply pow_nonneg. intuition order.
-Qed.
-
 (** Parity of power *)
 
 Lemma even_pow : forall a b, 0<b -> even (a^b) = even a.
@@ -86,7 +43,7 @@ Proof.
  rewrite 2 pow_2_r.
  now rewrite mul_opp_opp.
  assert (2*c < 0) by (apply mul_pos_neg; order').
- now rewrite !pow_neg.
+ now rewrite !pow_neg_r.
 Qed.
 
 Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
@@ -98,7 +55,7 @@ Proof.
  rewrite pow_opp_even by (now exists c).
  apply mul_opp_l.
  apply double_above in GT. rewrite mul_0_r in GT.
- rewrite !pow_neg by trivial. now rewrite opp_0.
+ rewrite !pow_neg_r by trivial. now rewrite opp_0.
 Qed.
 
 Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b.
@@ -126,7 +83,7 @@ Proof.
  assert (b~=0) by
   (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0).
  order.
- now rewrite pow_neg.
+ now rewrite pow_neg_r.
  rewrite abs_neq by order.
  rewrite pow_opp_odd; trivial.
  now rewrite mul_opp_opp, mul_1_l.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index ee75e4aa18..48d166c0ab 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -39,7 +39,7 @@ Proof.
  rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
 Qed.
 
-Lemma Zpow_neg : forall a b, b<0 -> Zpow a b = 0.
+Lemma Zpow_neg_r : forall a b, b<0 -> Zpow a b = 0.
 Proof.
  now destruct b.
 Qed.
@@ -171,7 +171,7 @@ Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow.
 
 Definition pow_0_r := Zpow_0_r.
 Definition pow_succ_r := Zpow_succ_r.
-Definition pow_neg := Zpow_neg.
+Definition pow_neg_r := Zpow_neg_r.
 Definition pow := Zpow.
 
 (** Sqrt *)
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index d632d22607..c2965016ad 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -261,7 +261,7 @@ Proof.
  simpl. unfold Zpower_pos; simpl. ring.
 Qed.
 
-Lemma pow_neg : forall a b, b<0 -> a^b == 0.
+Lemma pow_neg_r : forall a b, b<0 -> a^b == 0.
 Proof.
  intros a b. zify. intros Hb.
  destruct [b]; reflexivity || discriminate.
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index ea1f1bad62..db6e86ea7c 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -26,8 +26,13 @@ Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A).
  Declare Instance pow_wd : Proper (eq==>eq==>eq) pow.
  Axiom pow_0_r : forall a, a^0 == 1.
  Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b.
+ Axiom pow_neg_r : forall a b, b<0 -> a^b == 0.
 End NZPowSpec.
 
+(** The above [pow_neg_r] specification is useless (and trivially
+   provable) for N. Having it here allows to already derive
+   some slightly more general statements. *)
+
 Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A.
 Module Type NZPow' (A : NZOrdAxiomsSig) := Pow' A <+ NZPowSpec A.
 
@@ -83,10 +88,13 @@ Proof.
  now apply add_nonneg_nonneg.
 Qed.
 
-Lemma pow_mul_l : forall a b c, 0<=c ->
+Lemma pow_mul_l : forall a b c,
   (a*b)^c == a^c * b^c.
 Proof.
- intros a b c Hc. apply le_ind with (4:=Hc). solve_predicate_wd.
+ intros a b c.
+ destruct (lt_ge_cases c 0) as [Hc|Hc].
+ rewrite !(pow_neg_r _ _ Hc). now nzsimpl.
+ apply le_ind with (4:=Hc). solve_predicate_wd.
  now nzsimpl.
  clear c Hc. intros c Hc IH.
  nzsimpl; trivial.
@@ -106,9 +114,12 @@ Qed.
 
 (** Positivity *)
 
-Lemma pow_nonneg_nonneg : forall a b, 0<=a -> 0<=b -> 0<=a^b.
+Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b.
 Proof.
- intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ intros a b Ha.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ now rewrite !(pow_neg_r _ _ Hb).
+ apply le_ind with (4:=Hb). solve_predicate_wd.
  nzsimpl; order'.
  clear b Hb. intros b Hb IH.
  nzsimpl; trivial. now apply mul_nonneg_nonneg.
@@ -131,23 +142,28 @@ Proof.
  clear c Hc. intros c Hc IH (Ha,H).
  nzsimpl; try order.
  apply mul_lt_mono_nonneg; trivial.
- apply pow_nonneg_nonneg; try order.
+ apply pow_nonneg; try order.
  apply IH. now split.
 Qed.
 
-Lemma pow_le_mono_l : forall a b c, 0<=c -> 0<=a<=b -> a^c <= b^c.
+Lemma pow_le_mono_l : forall a b c, 0<=a<=b -> a^c <= b^c.
 Proof.
- intros a b c Hc (Ha,H).
- apply lt_eq_cases in Hc; destruct Hc as [Hc|Hc]; [|rewrite <- Hc].
+ intros a b c (Ha,H).
+ destruct (lt_trichotomy c 0) as [Hc|[Hc|Hc]].
+ rewrite !(pow_neg_r _ _ Hc); now nzsimpl.
+ rewrite Hc; now nzsimpl.
  apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H].
  apply lt_le_incl, pow_lt_mono_l; now try split.
- now nzsimpl.
 Qed.
 
-Lemma pow_gt_1 : forall a b, 1<a -> 0<b -> 1<a^b.
+Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b).
 Proof.
- intros a b Ha Hb. rewrite <- (pow_1_l b) by order.
+ intros a b Ha. split; intros Hb.
+ rewrite <- (pow_1_l b) by order.
  apply pow_lt_mono_l; try split; order'.
+ destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial.
+ rewrite pow_neg_r in Hb; order'.
+ rewrite H, pow_0_r in Hb. order.
 Qed.
 
 Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=b<c -> a^b < a^c.
@@ -165,9 +181,11 @@ Qed.
 
 (** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *)
 
-Lemma pow_le_mono_r : forall a b c, 0<a -> 0<=b<=c -> a^b <= a^c.
+Lemma pow_le_mono_r : forall a b c, 0<a -> b<=c -> a^b <= a^c.
 Proof.
- intros a b c Ha (Hb,H).
+ intros a b c Ha H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order.
  apply le_succ_l in Ha; rewrite <- one_succ in Ha.
  apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
  apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
@@ -175,7 +193,7 @@ Proof.
  nzsimpl; order.
 Qed.
 
-Lemma pow_le_mono : forall a b c d, 0<a<=c -> 0<=b<=d ->
+Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d ->
  a^b <= c^d.
 Proof.
  intros. transitivity (a^d).
@@ -237,7 +255,7 @@ Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
 Proof.
  intros a b c Ha Hb Hc.
  split; intro LE.
- apply pow_le_mono_l; try split; trivial. order.
+ apply pow_le_mono_l; try split; trivial.
  destruct (le_gt_cases a b) as [LE'|GT]; trivial.
  assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
  order.
@@ -299,10 +317,10 @@ Proof.
  apply add_le_mono.
  rewrite <- add_0_r at 1. apply add_le_mono_l.
   apply mul_nonneg_nonneg; trivial.
-  apply pow_nonneg_nonneg; trivial.
+  apply pow_nonneg; trivial.
  rewrite <- add_0_l at 1. apply add_le_mono_r.
   apply mul_nonneg_nonneg; trivial.
-  apply pow_nonneg_nonneg; trivial.
+  apply pow_nonneg; trivial.
  apply mul_le_mono_nonneg_l; trivial.
  now apply add_nonneg_nonneg.
 Qed.
@@ -343,7 +361,7 @@ Proof.
  assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order).
  rewrite EQ', <- !mul_assoc.
  apply mul_le_mono_nonneg_l.
- apply pow_nonneg_nonneg; order'.
+ apply pow_nonneg; order'.
  destruct (le_gt_cases a b).
  apply aux; try split; order'.
  rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)).
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index a40aa76579..d84748ee27 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -25,6 +25,7 @@ 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.
 
 Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A.
@@ -39,10 +40,10 @@ Module Type NZSqrtProp
 
 (** First, sqrt is non-negative *)
 
-Lemma sqrt_spec_nonneg : forall a b, 0<=a ->
+Lemma sqrt_spec_nonneg : forall a b,
  b*b <= a < S b * S b -> 0 <= b.
 Proof.
- intros a b Ha (LE,LT).
+ intros a b (LE,LT).
  destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso.
  assert (S b * S b < b * b).
   rewrite mul_succ_l, <- (add_0_r (b*b)).
@@ -52,18 +53,21 @@ Proof.
  order.
 Qed.
 
-Lemma sqrt_nonneg : forall a, 0<=a -> 0<=√a.
+Lemma sqrt_nonneg : forall a, 0<=√a.
 Proof.
- intros. now apply (sqrt_spec_nonneg a), sqrt_spec.
+ intros. destruct (lt_ge_cases a 0) as [Ha|Ha].
+ now rewrite (sqrt_neg _ Ha).
+ now apply (sqrt_spec_nonneg a), sqrt_spec.
 Qed.
 
 (** The spec of sqrt indeed determines it *)
 
-Lemma sqrt_unique : forall a b, 0<=a -> b*b<=a<(S b)*(S b) -> √a == b.
+Lemma sqrt_unique : forall a b, b*b <= a < S b * S b -> √a == b.
 Proof.
- intros a b Ha (LEb,LTb).
- assert (0<=b) by (apply (sqrt_spec_nonneg a); try split; trivial).
- assert (0<=√a) by now apply sqrt_nonneg.
+ intros a b (LEb,LTb).
+ assert (Ha : 0<=a) by (transitivity (b*b); trivial using square_nonneg).
+ assert (Hb : 0<=b) by (apply (sqrt_spec_nonneg a); now split).
+ assert (Ha': 0<=√a) by now apply sqrt_nonneg.
  destruct (sqrt_spec a Ha) as (LEa,LTa).
  assert (b <= √a).
   apply lt_succ_r, square_lt_simpl_nonneg; [|order].
@@ -80,16 +84,17 @@ Lemma sqrt_square : forall a, 0<=a -> √(a*a) == a.
 Proof.
  intros a Ha.
  apply sqrt_unique.
- apply square_nonneg.
  split. order.
  apply mul_lt_mono_nonneg; trivial using lt_succ_diag_r.
 Qed.
 
 (** Sqrt is a monotone function (but not a strict one) *)
 
-Lemma sqrt_le_mono : forall a b, 0<=a<=b -> √a <= √b.
+Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b.
 Proof.
- intros a b (Ha,Hab).
+ intros a b Hab.
+ destruct (lt_ge_cases a 0) as [Ha|Ha].
+ rewrite (sqrt_neg _ Ha). apply sqrt_nonneg.
  assert (Hb : 0 <= b) by order.
  destruct (sqrt_spec a Ha) as (LE,_).
  destruct (sqrt_spec b Hb) as (_,LT).
@@ -100,9 +105,12 @@ Qed.
 
 (** No reverse result for <=, consider for instance √2 <= √1 *)
 
-Lemma sqrt_lt_cancel : forall a b, 0<=a -> 0<=b -> √a < √b -> a < b.
+Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.
 Proof.
- intros a b Ha Hb H.
+ intros a b H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order.
+ destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|].
  destruct (sqrt_spec a Ha) as (_,LT).
  destruct (sqrt_spec b Hb) as (LE,_).
  apply le_succ_l in H.
@@ -119,7 +127,7 @@ Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b*b<=a <-> b <= √a).
 Proof.
  intros a b Ha Hb. split; intros H.
  rewrite <- (sqrt_square b); trivial.
- apply sqrt_le_mono. split. apply square_nonneg. trivial.
+ now apply sqrt_le_mono.
  destruct (sqrt_spec a Ha) as (LE,LT).
  transitivity (√a * √a); trivial.
  now apply mul_le_mono_nonneg.
@@ -133,8 +141,7 @@ Proof.
  destruct (sqrt_spec a Ha) as (LE,_).
  apply square_lt_simpl_nonneg; try order.
  rewrite <- (sqrt_square b Hb) in H.
- apply sqrt_lt_cancel; trivial.
- apply square_nonneg.
+ now apply sqrt_lt_cancel.
 Qed.
 
 (** Sqrt and basic constants *)
@@ -151,7 +158,7 @@ Qed.
 
 Lemma sqrt_2 : √2 == 1.
 Proof.
- apply sqrt_unique. order'. nzsimpl. split. order'.
+ apply sqrt_unique. nzsimpl. split. order'.
  apply lt_succ_r, lt_le_incl, lt_succ_r. nzsimpl'; order.
 Qed.
 
@@ -178,11 +185,15 @@ Qed.
 (** Due to rounding error, we don't have the usual √(a*b) = √a*√b
     but only lower and upper bounds. *)
 
-Lemma sqrt_mul_below : forall a b, 0<=a -> 0<=b -> √a * √b <= √(a*b).
+Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
 Proof.
- intros a b Ha Hb.
- assert (Ha':=sqrt_nonneg _ Ha).
- assert (Hb':=sqrt_nonneg _ Hb).
+ intros a b.
+ destruct (lt_ge_cases a 0) as [Ha|Ha].
+ rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg.
+ assert (Ha':=sqrt_nonneg a).
+ assert (Hb':=sqrt_nonneg b).
  apply sqrt_le_square; try now apply mul_nonneg_nonneg.
  rewrite mul_shuffle1.
  apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg.
@@ -190,8 +201,7 @@ Proof.
   now apply sqrt_spec.
 Qed.
 
-Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b ->
- √(a*b) < S (√a) * S (√b).
+Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b).
 Proof.
  intros a b Ha Hb.
  apply sqrt_lt_square.
@@ -211,11 +221,19 @@ Qed.
 
 (** Sqrt and addition *)
 
-Lemma sqrt_add_le : forall a b, 0<=a -> 0<=b -> √(a+b) <= √a + √b.
+Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.
 Proof.
- intros a b Ha Hb.
- assert (Ha':=sqrt_nonneg _ Ha).
- assert (Hb':=sqrt_nonneg _ Hb).
+ assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b).
+  intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl.
+  apply sqrt_le_mono.
+  rewrite <- (add_0_l b) at 2.
+  apply add_le_mono_r; order.
+ intros a b.
+ destruct (lt_ge_cases a 0) as [Ha|Ha]. now apply AUX.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+  rewrite (add_comm a), (add_comm (√a)); now apply AUX.
+ assert (Ha':=sqrt_nonneg a).
+ assert (Hb':=sqrt_nonneg b).
  rewrite <- lt_succ_r.
  apply sqrt_lt_square.
   now apply add_nonneg_nonneg.
@@ -241,8 +259,8 @@ Qed.
 Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> √a + √b <= √(2*(a+b)).
 Proof.
  intros a b Ha Hb.
- assert (Ha':=sqrt_nonneg _ Ha).
- assert (Hb':=sqrt_nonneg _ Hb).
+ assert (Ha':=sqrt_nonneg a).
+ assert (Hb':=sqrt_nonneg b).
  apply sqrt_le_square.
   apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg.
   now apply add_nonneg_nonneg.
diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index 92e90b9c80..4a9cf536be 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 ec0fa89bff..60a836d416 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 348eee5ed2..8b7b06966f 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 b91b43e310..de5ef47872 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 f072fc24aa..f242951e54 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.