Numbers: axiomatization + generic properties of abs and sgn.

 This allow to really finish files about division.
 An abs and sgn is added to BigZ.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12644 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 1 deletions

diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 516827616..6a2745d34 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -18,7 +18,7 @@ Local Open Scope Z_scope.
 
 (** * Implementation of [ZAxiomsSig] by [BinInt.Z] *)
 
-Module ZBinAxiomsMod <: ZAxiomsSig.
+Module ZBinAxiomsMod <: ZAxiomsExtSig.
 
 (** Bi-directional induction. *)
 
@@ -70,6 +70,18 @@ Definition succ_pred n := eq_sym (Zsucc_pred n).
 Definition opp_0 := Zopp_0.
 Definition opp_succ := Zopp_succ.
 
+(** Absolute value and sign *)
+
+Definition abs_eq := Zabs_eq.
+Definition abs_neq := Zabs_non_eq.
+
+Lemma sgn_null : forall x, x = 0 -> Zsgn x = 0.
+Proof. intros. apply <- Zsgn_null; auto. Qed.
+Lemma sgn_pos : forall x, 0 < x -> Zsgn x = 1.
+Proof. intros. apply <- Zsgn_pos; auto. Qed.
+Lemma sgn_neg : forall x, x < 0 -> Zsgn x = -1.
+Proof. intros. apply <- Zsgn_neg; auto. Qed.
+
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
 
@@ -86,6 +98,8 @@ Definition le := Zle.
 Definition min := Zmin.
 Definition max := Zmax.
 Definition opp := Zopp.
+Definition abs := Zabs.
+Definition sgn := Zsgn.
 
 End ZBinAxiomsMod.