# Library Coq.ZArith.Znat

Binary Integers (Pierre Crégut, CNET, Lannion, France)
Require Export Arith_base.
Require Import BinPos.
Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
Require Import Decidable.
Require Import Peano_dec.
Require Import Min Max Zmin Zmax.
Require Export Compare_dec.
Open Local Scope Z_scope.
Definition neq (x y:nat) := x <> y.
Properties of the injection from nat into Z
Injection and successor
Theorem inj_0 : Z_of_nat 0 = 0%Z.
Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
Injection and equality.
Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
Injection and order relations:
One way ...
Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m.
Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
The other way ...
Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m.
Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
Injection and usual operations
Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
Theorem inj_minus1 :
forall n m:nat, (m <= n)%nat -> Z_of_nat (n - m) = Z_of_nat n - Z_of_nat m.
Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0.
Theorem inj_minus : forall n m:nat,
Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
Theorem inj_min : forall n m:nat,
Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
Theorem inj_max : forall n m:nat,
Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
Composition of injections
Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
Misc
Theorem intro_Z :
forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
Lemma Zpos_P_of_succ_nat : forall n:nat,
Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).