2 files changed, 17 insertions, 6 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index b33ed5f8ef..be201f2d66 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -38,6 +38,7 @@ Module Type ZType.
  Parameter max : t -> t -> t.
  Parameter zero : t.
  Parameter one : t.
+ Parameter two : t.
  Parameter minus_one : t.
  Parameter succ : t -> t.
  Parameter add  : t -> t -> t.
@@ -65,6 +66,7 @@ Module Type ZType.
  Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
+ Parameter spec_2: [two] = 2.
  Parameter spec_m1: [minus_one] = -1.
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
@@ -94,6 +96,8 @@ Module Type ZType_Notation (Import Z:ZType).
  Notation "[ x ]" := (to_Z x).
  Infix "=="  := eq (at level 70).
  Notation "0" := zero.
+ Notation "1" := one.
+ Notation "2" := two.
  Infix "+" := add.
  Infix "-" := sub.
  Infix "*" := mul.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 90bda6343e..3e63755434 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -17,7 +17,7 @@ Require Import ZArith Nnat ZAxioms ZDivFloor ZSig.
 Module ZTypeIsZAxioms (Import Z : ZType').
 
 Hint Rewrite
- spec_0 spec_1 spec_add spec_sub spec_pred spec_succ
+ spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
  spec_pow spec_even spec_odd
@@ -43,6 +43,16 @@ Proof.
 intros. zify. auto with zarith.
 Qed.
 
+Theorem one_succ : 1 == succ 0.
+Proof.
+now zify.
+Qed.
+
+Theorem two_succ : 2 == succ 1.
+Proof.
+now zify.
+Qed.
+
 Section Induction.
 
 Variable A : Z.t -> Prop.
@@ -225,12 +235,12 @@ Proof.
 intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0.
+Theorem sgn_pos : forall n, 0<n -> sgn n == 1.
 Proof.
 intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0).
+Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1.
 Proof.
 intros n. zify. omega with *.
 Qed.
@@ -239,9 +249,6 @@ Qed.
 
 Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
 
-Local Notation "1" := (succ 0).
-Local Notation "2" := (succ 1).
-
 Lemma pow_0_r : forall a, a^0 == 1.
 Proof.
  intros. now zify.