diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-08 09:54:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-08 09:54:31 +0000 |
| commit | c08b8247aec05b34a908663aa160fdbd617b8220 (patch) | |
| tree | 58bf890038871e9538cbc0d4be66374571adbaed /theories/ZArith/Zabs.v | |
| parent | 9a57002cd644bac29e0ad338756d1a01613e6c13 (diff) | |
setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.
A file ZOdiv is added which contains results about this euclidean division.
Interest compared with Zdiv: ZOdiv implements others (better?) conventions
concerning negative numbers, in particular it is compatible with Caml
div and mod.
ZOdiv is only partially finished...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zabs.v')
| -rw-r--r-- | theories/ZArith/Zabs.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index ab699f4a7..a52df1bfc 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -207,3 +207,19 @@ Lemma Zsgn_spec : forall x:Z, Proof. intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition. Qed. + +Lemma Zsgn_pos : forall x:Z, Zsgn x = 1 <-> 0 < x. +Proof. + destruct x; now intuition. +Qed. + +Lemma Zsgn_neg : forall x:Z, Zsgn x = -1 <-> x < 0. +Proof. + destruct x; now intuition. +Qed. + +Lemma Zsgn_null : forall x:Z, Zsgn x = 0 <-> x = 0. +Proof. + destruct x; now intuition. +Qed. + |