diff options
| author | letouzey | 2010-11-02 15:10:31 +0000 |
|---|---|---|
| committer | letouzey | 2010-11-02 15:10:31 +0000 |
| commit | 11f5deaf28c489f54d86d8f38314bb77544f70b7 (patch) | |
| tree | c5c32c3169033fa93d49b900d96eaa4c50c5936a /theories/Numbers/Integer/Binary | |
| parent | 2e93411329de51cac30c63e111a03059bde43394 (diff) | |
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
Diffstat (limited to 'theories/Numbers/Integer/Binary')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 *) |