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).