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/SpecViaZ | |
| 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/SpecViaZ')
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |