diff options
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. |