diff options
Diffstat (limited to 'theories/ZArith/Zabs.v')
| -rw-r--r-- | theories/ZArith/Zabs.v | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index c7f0bb723..e43d68bfa 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -7,7 +7,7 @@ (************************************************************************) (*i $Id$ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) Require Import Arith_base. Require Import BinPos. @@ -70,6 +70,13 @@ Proof. (intros H2; rewrite H2); auto. Qed. +Lemma Zabs_spec : forall x:Z, + 0 <= x /\ Zabs x = x \/ + 0 > x /\ Zabs x = -x. +Proof. + intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate. +Qed. + (** * Triangular inequality *) Hint Local Resolve Zle_neg_pos: zarith. @@ -89,6 +96,16 @@ Proof. apply Zplus_le_compat; simpl in |- *; auto with zarith. Qed. +(** * A characterization of the sign function: *) + +Lemma Zsgn_spec : forall x:Z, + 0 < x /\ Zsgn x = 1 \/ + 0 = x /\ Zsgn x = 0 \/ + 0 > x /\ Zsgn x = -1. +Proof. + intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition. +Qed. + (** * Absolute value and multiplication *) Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n. |