# Binary Integers

Initial author: Pierre CrÃ©gut, CNET, Lannion, France
The type Z and its constructors Z0 and Zpos and Zneg are now defined in BinNums.v

Local Open Scope Z_scope.

Every definitions and early properties about binary integers are placed in a module Z for qualification purpose.

# Definitions of operations, now in a separate file

Include BinIntDef.Z.

When including property functors, only inline t eq zero one two

# Logic Predicates

Definition eq := @Logic.eq Z.
Definition eq_equiv := @eq_equivalence Z.

Definition lt x y := (x ?= y) = Lt.
Definition gt x y := (x ?= y) = Gt.
Definition le x y := (x ?= y) <> Gt.
Definition ge x y := (x ?= y) <> Lt.

Infix "<=" := le : Z_scope.
Infix "<" := lt : Z_scope.
Infix ">=" := ge : Z_scope.
Infix ">" := gt : Z_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.

Definition divide x y := exists z, y = z*x.
Notation "( x | y )" := (divide x y) (at level 0).

Definition Even a := exists b, a = 2*b.
Definition Odd a := exists b, a = 2*b+1.

# Decidability of equality.

Definition eq_dec (x y : Z) : {x = y} + {x <> y}.

# Properties of pos_sub

pos_sub can be written in term of positive comparison and subtraction (cf. earlier definition of addition of Z)

Lemma pos_sub_spec p q :
pos_sub p q =
match (p ?= q)%positive with
| Eq => 0
| Lt => Zneg (q - p)
| Gt => Zpos (p - q)
end.

Particular cases of the previous result

Lemma pos_sub_diag p : pos_sub p p = 0.

Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = Zneg (q - p).

Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = Zpos (p - q).

The opposite of pos_sub is pos_sub with reversed arguments

Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p.

# Results concerning Zpos and Zneg and the operators

Lemma opp_Zneg p : - Zneg p = Zpos p.

Lemma opp_Zpos p : - Zpos p = Zneg p.

Lemma succ_Zpos p : succ (Zpos p) = Zpos (Pos.succ p).

Lemma add_Zpos p q : Zpos p + Zpos q = Zpos (p+q).

Lemma add_Zneg p q : Zneg p + Zneg q = Zneg (p+q).

Lemma add_Zpos_Zneg p q : Zpos p + Zneg q = pos_sub p q.

Lemma add_Zneg_Zpos p q : Zneg p + Zpos q = pos_sub q p.

Lemma sub_Zpos n m : (n < m)%positive -> Zpos m - Zpos n = Zpos (m-n).

Lemma mul_Zpos (p q : positive) : Zpos p * Zpos q = Zpos (p*q).

Lemma pow_Zpos p q : (Zpos p)^(Zpos q) = Zpos (p^q).

Lemma inj_Zpos p q : Zpos p = Zpos q <-> p = q.

Lemma inj_Zneg p q : Zneg p = Zneg q <-> p = q.

Lemma pos_xI p : Zpos p~1 = 2 * Zpos p + 1.

Lemma pos_xO p : Zpos p~0 = 2 * Zpos p.

Lemma neg_xI p : Zneg p~1 = 2 * Zneg p - 1.

Lemma neg_xO p : Zneg p~0 = 2 * Zneg p.

In the following module, we group results that are needed now to prove specifications of operations, but will also be provided later by the generic functor of properties.

Module Import Private_BootStrap.

## Zero is neutral for addition

Lemma add_0_r n : n + 0 = n.

Lemma add_comm n m : n + m = m + n.

Lemma opp_add_distr n m : - (n + m) = - n + - m.

## Opposite is injective

Lemma opp_inj n m : -n = -m -> n = m.

Lemma pos_sub_add p q r :
pos_sub (p + q) r = Zpos p + pos_sub q r.

Lemma add_assoc n m p : n + (m + p) = n + m + p.

## Subtraction and successor

Lemma sub_succ_l n m : succ n - m = succ (n - m).

## Opposite is inverse for addition

Lemma add_opp_diag_r n : n + - n = 0.

Lemma add_opp_diag_l n : - n + n = 0.

## Commutativity of multiplication

Lemma mul_comm n m : n * m = m * n.

## Associativity of multiplication

Lemma mul_assoc n m p : n * (m * p) = n * m * p.

Multiplication and constants

Lemma mul_1_l n : 1 * n = n.

Lemma mul_1_r n : n * 1 = n.

## Multiplication and Opposite

Lemma mul_opp_l n m : - n * m = - (n * m).

Lemma mul_opp_r n m : n * - m = - (n * m).

Lemma mul_opp_opp n m : - n * - m = n * m.

Lemma mul_opp_comm n m : - n * m = n * - m.

## Distributivity of multiplication over addition

Lemma mul_add_distr_pos (p:positive) n m :
Zpos p * (n + m) = Zpos p * n + Zpos p * m.

Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p.

Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p.

End Private_BootStrap.

# Proofs of specifications

## Specification of constants

Lemma one_succ : 1 = succ 0.

Lemma two_succ : 2 = succ 1.

Lemma add_0_l n : 0 + n = n.

Lemma add_succ_l n m : succ n + m = succ (n + m).

## Specification of opposite

Lemma opp_0 : -0 = 0.

Lemma opp_succ n : -(succ n) = pred (-n).

## Specification of successor and predecessor

Lemma succ_pred n : succ (pred n) = n.

Lemma pred_succ n : pred (succ n) = n.

## Specification of subtraction

Lemma sub_0_r n : n - 0 = n.

Lemma sub_succ_r n m : n - succ m = pred (n - m).

## Specification of multiplication

Lemma mul_0_l n : 0 * n = 0.

Lemma mul_succ_l n m : succ n * m = n * m + m.

## Specification of comparisons and order

Lemma eqb_eq n m : (n =? m) = true <-> n = m.

Lemma ltb_lt n m : (n <? m) = true <-> n < m.

Lemma leb_le n m : (n <=? m) = true <-> n <= m.

Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.

Lemma compare_sub n m : (n ?= m) = (n - m ?= 0).

Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).

Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.

Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.

Some more advanced properties of comparison and orders, including compare_spec and lt_irrefl and lt_eq_cases.

Include BoolOrderFacts.

Remaining specification of lt and le

Lemma lt_succ_r n m : n < succ m <-> n<=m.

## Specification of minimum and maximum

Lemma max_l n m : m<=n -> max n m = n.

Lemma max_r n m : n<=m -> max n m = m.

Lemma min_l n m : n<=m -> min n m = n.

Lemma min_r n m : m<=n -> min n m = m.

## Specification of absolute value

Lemma abs_eq n : 0 <= n -> abs n = n.

Lemma abs_neq n : n <= 0 -> abs n = - n.

## Specification of sign

Lemma sgn_null n : n = 0 -> sgn n = 0.

Lemma sgn_pos n : 0 < n -> sgn n = 1.

Lemma sgn_neg n : n < 0 -> sgn n = -1.

## Specification of power

Lemma pow_0_r n : n^0 = 1.

Lemma pow_succ_r n m : 0<=m -> n^(succ m) = n * n^m.

Lemma pow_neg_r n m : m<0 -> n^m = 0.

For folding back a pow_pos into a pow

Lemma pow_pos_fold n p : pow_pos n p = n ^ (Zpos p).

## Specification of square

Lemma square_spec n : square n = n * n.

## Specification of square root

Lemma sqrtrem_spec n : 0<=n ->
let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.

Lemma sqrt_spec n : 0<=n ->
let s := sqrt n in s*s <= n < (succ s)*(succ s).

Lemma sqrt_neg n : n<0 -> sqrt n = 0.

Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.

## Specification of logarithm

Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)).

Lemma log2_nonpos n : n<=0 -> log2 n = 0.

Specification of parity functions

Lemma even_spec n : even n = true <-> Even n.

Lemma odd_spec n : odd n = true <-> Odd n.

## Multiplication and Doubling

Lemma double_spec n : double n = 2*n.

Lemma succ_double_spec n : succ_double n = 2*n + 1.

Lemma pred_double_spec n : pred_double n = 2*n - 1.

## Correctness proofs for Trunc division

Lemma pos_div_eucl_eq a b : 0 < b ->
let (q, r) := pos_div_eucl a b in Zpos a = q * b + r.

Lemma div_eucl_eq a b : b<>0 ->
let (q, r) := div_eucl a b in a = b * q + r.

Lemma div_mod a b : b<>0 -> a = b*(a/b) + (a mod b).

Lemma pos_div_eucl_bound a b : 0<b -> 0 <= snd (pos_div_eucl a b) < b.

Lemma mod_pos_bound a b : 0 < b -> 0 <= a mod b < b.

Definition mod_bound_pos a b (_:0<=a) := mod_pos_bound a b.

Lemma mod_neg_bound a b : b < 0 -> b < a mod b <= 0.

## Correctness proofs for Floor division

Theorem quotrem_eq a b : let (q,r) := quotrem a b in a = q * b + r.

Lemma quot_rem' a b : a = b*(aÃ·b) + rem a b.

Lemma quot_rem a b : b<>0 -> a = b*(aÃ·b) + rem a b.

Lemma rem_bound_pos a b : 0<=a -> 0<b -> 0 <= rem a b < b.

Lemma rem_opp_l' a b : rem (-a) b = - (rem a b).

Lemma rem_opp_r' a b : rem a (-b) = rem a b.

Lemma rem_opp_l a b : b<>0 -> rem (-a) b = - (rem a b).

Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b.

## Correctness proofs for gcd

Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.

Lemma ggcd_correct_divisors a b :
let '(g,(aa,bb)) := ggcd a b in
a = g*aa /\ b = g*bb.

Lemma gcd_divide_l a b : (gcd a b | a).

Lemma gcd_divide_r a b : (gcd a b | b).

Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b).

Lemma gcd_nonneg a b : 0 <= gcd a b.

ggcd and opp : an auxiliary result used in QArith

Theorem ggcd_opp a b :
ggcd (-a) b = (let '(g,(aa,bb)) := ggcd a b in (g,(-aa,bb))).

## Conversions between Z.testbit and N.testbit

Lemma testbit_of_N a n :
testbit (of_N a) (of_N n) = N.testbit a n.

Lemma testbit_of_N' a n : 0<=n ->
testbit (of_N a) n = N.testbit a (to_N n).

Lemma testbit_Zpos a n : 0<=n ->
testbit (Zpos a) n = N.testbit (Npos a) (to_N n).

Lemma testbit_Zneg a n : 0<=n ->
testbit (Zneg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)).

## Proofs of specifications for bitwise operations

Lemma div2_spec a : div2 a = shiftr a 1.

Lemma testbit_0_l n : testbit 0 n = false.

Lemma testbit_neg_r a n : n<0 -> testbit a n = false.

Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.

Lemma testbit_odd_succ a n : 0<=n ->
testbit (2*a+1) (succ n) = testbit a n.

Lemma testbit_even_succ a n : 0<=n ->
testbit (2*a) (succ n) = testbit a n.

Correctness proofs about Z.shiftr and Z.shiftl

Lemma shiftr_spec_aux a n m : 0<=n -> 0<=m ->
testbit (shiftr a n) m = testbit a (m+n).

Lemma shiftl_spec_low a n m : m<n ->
testbit (shiftl a n) m = false.

Lemma shiftl_spec_high a n m : 0<=m -> n<=m ->
testbit (shiftl a n) m = testbit a (m-n).

Lemma shiftr_spec a n m : 0<=m ->
testbit (shiftr a n) m = testbit a (m+n).

Correctness proofs for bitwise operations

Lemma lor_spec a b n :
testbit (lor a b) n = testbit a n || testbit b n.

Lemma land_spec a b n :
testbit (land a b) n = testbit a n && testbit b n.

Lemma ldiff_spec a b n :
testbit (ldiff a b) n = testbit a n && negb (testbit b n).

Lemma lxor_spec a b n :
testbit (lxor a b) n = xorb (testbit a n) (testbit b n).

## Induction principles based on successor / predecessor

Lemma peano_ind (P : Z -> Prop) :
P 0 ->
(forall x, P x -> P (succ x)) ->
(forall x, P x -> P (pred x)) ->
forall z, P z.

Lemma bi_induction (P : Z -> Prop) :
Proper (eq ==> iff) P ->
P 0 ->
(forall x, P x <-> P (succ x)) ->
forall z, P z.

# Proofs of morphisms, obvious since eq is Leibniz

Local Obligation Tactic := simpl_relation.
Program Definition succ_wd : Proper (eq==>eq) succ := _.
Program Definition pred_wd : Proper (eq==>eq) pred := _.
Program Definition opp_wd : Proper (eq==>eq) opp := _.
Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.

Include ZProp
<+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Otherwise Z stays associated with abstract_scope : (TODO FIX)

In generic statements, the predicates lt and le have been favored, whereas gt and ge don't even exist in the abstract layers. The use of gt and ge is hence not recommended. We provide here the bare minimal results to related them with lt and le.

Lemma gt_lt_iff n m : n > m <-> m < n.

Lemma gt_lt n m : n > m -> m < n.

Lemma lt_gt n m : n < m -> m > n.

Lemma ge_le_iff n m : n >= m <-> m <= n.

Lemma ge_le n m : n >= m -> m <= n.

Lemma le_ge n m : n <= m -> m >= n.

We provide a tactic converting from one style to the other.

Ltac swap_greater := rewrite ?gt_lt_iff in *; rewrite ?ge_le_iff in *.

Similarly, the boolean comparisons ltb and leb are favored over their dual gtb and geb. We prove here the equivalence and a few minimal results.

Lemma gtb_ltb n m : (n >? m) = (m <? n).

Lemma geb_leb n m : (n >=? m) = (m <=? n).

Lemma gtb_lt n m : (n >? m) = true <-> m < n.

Lemma geb_le n m : (n >=? m) = true <-> m <= n.

Lemma gtb_spec n m : BoolSpec (m<n) (n<=m) (n >? m).

Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m).

TODO : to add in Numbers ?

Lemma add_reg_l n m p : n + m = n + p -> m = p.

Lemma mul_reg_l n m p : p <> 0 -> p * n = p * m -> n = m.

Lemma mul_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.

Lemma opp_eq_mul_m1 n : - n = n * -1.

Lemma add_diag n : n + n = 2 * n.

# Comparison and opposite

Lemma compare_opp n m : (- n ?= - m) = (m ?= n).

Lemma add_compare_mono_l n m p : (n + m ?= n + p) = (m ?= p).

End Z.

Export Notations

Infix "+" := Z.add : Z_scope.
Notation "- x" := (Z.opp x) : Z_scope.
Infix "-" := Z.sub : Z_scope.
Infix "*" := Z.mul : Z_scope.
Infix "^" := Z.pow : Z_scope.
Infix "/" := Z.div : Z_scope.
Infix "mod" := Z.modulo (at level 40, no associativity) : Z_scope.
Infix "Ã·" := Z.quot (at level 40, left associativity) : Z_scope.

Notation "( x | y )" := (Z.divide x y) (at level 0).

Infix "?=" := Z.compare (at level 70, no associativity) : Z_scope.

Infix "<=" := Z.le : Z_scope.
Infix "<" := Z.lt : Z_scope.
Infix ">=" := Z.ge : Z_scope.
Infix ">" := Z.gt : Z_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.

Infix "=?" := Z.eqb (at level 70, no associativity) : Z_scope.
Infix "<=?" := Z.leb (at level 70, no associativity) : Z_scope.
Infix "<?" := Z.ltb (at level 70, no associativity) : Z_scope.
Infix ">=?" := Z.geb (at level 70, no associativity) : Z_scope.
Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope.

Compatibility Notations

Notation Zdouble_plus_one := Z.succ_double (only parsing).
Notation Zdouble_minus_one := Z.pred_double (only parsing).
Notation Zdouble := Z.double (only parsing).
Notation ZPminus := Z.pos_sub (only parsing).
Notation Zsucc' := Z.succ (only parsing).
Notation Zpred' := Z.pred (only parsing).
Notation Zplus' := Z.add (only parsing).
Notation Zplus := Z.add (only parsing). Notation Zopp := Z.opp (only parsing).
Notation Zsucc := Z.succ (only parsing).
Notation Zpred := Z.pred (only parsing).
Notation Zminus := Z.sub (only parsing).
Notation Zmult := Z.mul (only parsing).
Notation Zcompare := Z.compare (only parsing).
Notation Zsgn := Z.sgn (only parsing).
Notation Zle := Z.le (only parsing).
Notation Zge := Z.ge (only parsing).
Notation Zlt := Z.lt (only parsing).
Notation Zgt := Z.gt (only parsing).
Notation Zmax := Z.max (only parsing).
Notation Zmin := Z.min (only parsing).
Notation Zabs := Z.abs (only parsing).
Notation Zabs_nat := Z.abs_nat (only parsing).
Notation Zabs_N := Z.abs_N (only parsing).
Notation Z_of_nat := Z.of_nat (only parsing).
Notation Z_of_N := Z.of_N (only parsing).

Notation Zind := Z.peano_ind (only parsing).
Notation Zopp_0 := Z.opp_0 (only parsing).
Notation Zopp_neg := Z.opp_Zneg (only parsing).
Notation Zopp_involutive := Z.opp_involutive (only parsing).
Notation Zopp_inj := Z.opp_inj (only parsing).
Notation Zplus_0_l := Z.add_0_l (only parsing).
Notation Zplus_0_r := Z.add_0_r (only parsing).
Notation Zplus_comm := Z.add_comm (only parsing).
Notation Zopp_plus_distr := Z.opp_add_distr (only parsing).
Notation Zopp_succ := Z.opp_succ (only parsing).
Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing).
Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing).
Notation Zplus_assoc := Z.add_assoc (only parsing).
Notation Zplus_permute := Z.add_shuffle3 (only parsing).
Notation Zplus_reg_l := Z.add_reg_l (only parsing).
Notation Zplus_succ_l := Z.add_succ_l (only parsing).
Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
Notation Zsucc_inj := Z.succ_inj (only parsing).
Notation Zsucc'_inj := Z.succ_inj (only parsing).
Notation Zsucc'_pred' := Z.succ_pred (only parsing).
Notation Zpred'_succ' := Z.pred_succ (only parsing).
Notation Zpred'_inj := Z.pred_inj (only parsing).
Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing).
Notation Zminus_0_r := Z.sub_0_r (only parsing).
Notation Zminus_diag := Z.sub_diag (only parsing).
Notation Zminus_plus_distr := Z.sub_add_distr (only parsing).
Notation Zminus_succ_r := Z.sub_succ_r (only parsing).
Notation Zminus_plus := Z.add_simpl_l (only parsing).
Notation Zmult_0_l := Z.mul_0_l (only parsing).
Notation Zmult_0_r := Z.mul_0_r (only parsing).
Notation Zmult_1_l := Z.mul_1_l (only parsing).
Notation Zmult_1_r := Z.mul_1_r (only parsing).
Notation Zmult_comm := Z.mul_comm (only parsing).
Notation Zmult_assoc := Z.mul_assoc (only parsing).
Notation Zmult_permute := Z.mul_shuffle3 (only parsing).
Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing).
Notation Zdouble_mult := Z.double_spec (only parsing).
Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing).
Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing).
Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing).
Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing).
Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing).
Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing).
Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing).
Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing).
Notation Zmult_reg_l := Z.mul_reg_l (only parsing).
Notation Zmult_reg_r := Z.mul_reg_r (only parsing).
Notation Zmult_succ_l := Z.mul_succ_l (only parsing).
Notation Zmult_succ_r := Z.mul_succ_r (only parsing).
Notation Zpos_xI := Z.pos_xI (only parsing).
Notation Zpos_xO := Z.pos_xO (only parsing).
Notation Zneg_xI := Z.neg_xI (only parsing).
Notation Zneg_xO := Z.neg_xO (only parsing).

Notation Z := Z (only parsing).
Notation Z_rect := Z_rect (only parsing).
Notation Z_rec := Z_rec (only parsing).
Notation Z_ind := Z_ind (only parsing).
Notation Z0 := Z0 (only parsing).
Notation Zpos := Zpos (only parsing).
Notation Zneg := Zneg (only parsing).

Compatibility lemmas. These could be notations, but scope information would be lost.

Notation SYM1 lem := (fun n => eq_sym (lem n)).
Notation SYM2 lem := (fun n m => eq_sym (lem n m)).
Notation SYM3 lem := (fun n m p => eq_sym (lem n m p)).

Lemma Zplus_assoc_reverse : forall n m p, n+m+p = n+(m+p).
Lemma Zplus_succ_r_reverse : forall n m, Z.succ (n+m) = n+Z.succ m.
Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
Lemma Zplus_0_r_reverse : forall n, n = n + 0.
Lemma Zplus_eq_compat : forall n m p q, n=m -> p=q -> n+p=m+q.
Lemma Zpos_succ_morphism : forall p, Zpos (Psucc p) = Zsucc (Zpos p).
Lemma Zsucc_pred : forall n, n = Z.succ (Z.pred n).
Lemma Zpred_succ : forall n, n = Z.pred (Z.succ n).
Lemma Zsucc_eq_compat : forall n m, n = m -> Z.succ n = Z.succ m.
Lemma Zminus_0_l_reverse : forall n, n = n - 0.
Lemma Zminus_diag_reverse : forall n, 0 = n-n.
Lemma Zminus_succ_l : forall n m, Z.succ (n - m) = Z.succ n - m.
Lemma Zplus_minus_eq : forall n m p, n = m + p -> p = n - m.
Lemma Zplus_minus : forall n m, n + (m - n) = m.
Lemma Zminus_plus_simpl_l : forall n m p, p + n - (p + m) = n - m.
Lemma Zminus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
Lemma Zminus_plus_simpl_r : forall n m p, n + p - (m + p) = n - m.
Lemma Zpos_minus_morphism : forall a b,
Pcompare a b Eq = Lt -> Zpos (b - a) = Zpos b - Zpos a.
Lemma Zeq_minus : forall n m, n = m -> n - m = 0.
Lemma Zminus_eq : forall n m, n - m = 0 -> n = m.
Lemma Zpos_mult_morphism : forall p q, Zpos (p * q) = Zpos p * Zpos q.
Lemma Zmult_0_r_reverse : forall n, 0 = n * 0.
Lemma Zmult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
Lemma Zmult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
Lemma Zmult_integral_l : forall n m, n <> 0 -> m * n = 0 -> m = 0.
Lemma Zopp_mult_distr_l : forall n m, - (n * m) = - n * m.
Lemma Zopp_mult_distr_r : forall n m, - (n * m) = n * - m.
Lemma Zmult_minus_distr_l : forall n m p, p * (n - m) = p * n - p * m.
Lemma Zmult_succ_r_reverse : forall n m, n * m + n = n * Zsucc m.
Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Zsucc n * m.
Lemma Zpos_eq : forall p q, p = q -> Zpos p = Zpos q.
Lemma Zpos_eq_rev : forall p q, Zpos p = Zpos q -> p = q.
Lemma Zpos_eq_iff : forall p q, p = q <-> Zpos p = Zpos q.
Lemma Zpos_plus_distr : forall p q, Zpos (p + q) = Zpos p + Zpos q.
Lemma Zneg_plus_distr : forall p q, Zneg (p + q) = Zneg p + Zneg q.

Hint Immediate Zsucc_pred: zarith.

Obsolete stuff

Definition Zne (x y:Z) := x <> y.
Ltac elim_compare com1 com2 :=
case (Dcompare (com1 ?= com2)%Z);
[ idtac | let x := fresh "H" in
(intro x; case x; clear x) ].

Lemma ZL0 : 2%nat = (1 + 1)%nat.

Lemma Zplus_diag_eq_mult_2 n : n + n = n * 2.

Lemma Z_eq_mult n m : m = 0 -> m * n = 0.