diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:31 +0000 |
| commit | 11f5deaf28c489f54d86d8f38314bb77544f70b7 (patch) | |
| tree | c5c32c3169033fa93d49b900d96eaa4c50c5936a /theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | |
| 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/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 12 |
1 files changed, 12 insertions, 0 deletions
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. |