Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Export NumPrelude NZAxioms.
Require Import NZBase NZOrder NZAddOrder Plus Minus.

In this file, we investigate the shape of domains satisfying the NZDomainSig interface. In particular, we define a translation from Peano numbers nat into NZ.

Local Notation "f ^ n" := (fun x => nat_rect _ x (fun _ => f) n).

Instance nat_rect_wd n {A} (R:relation A) :
 Proper (R==>(R==>R)==>R) (fun x f => nat_rect (fun _ => _) x (fun _ => f) n).n:nat
A:Type
R:relation A
Proper (R ==> (R ==> R) ==> R)
  (fun (x : A) (f : A -> A) =>
   nat_rect (fun _ : nat => A) x (fun _ : nat => f) n)
Proof.n:nat
A:Type
R:relation A
Proper (R ==> (R ==> R) ==> R)
  (fun (x : A) (f : A -> A) =>
   nat_rect (fun _ : nat => A) x (fun _ : nat => f) n)
intros x y eq_xy f g eq_fg; induction n; [assumption | now apply eq_fg].
Qed.

Module NZDomainProp (Import NZ:NZDomainSig').
Include NZBaseProp NZ.

Relationship between points thanks to succ and pred.

For any two points, one is an iterated successor of the other.

Lemma itersucc_or_itersucc n m : exists k, n == (S^k) m \/ m == (S^k) n.n, m:t
exists k : nat, n == (S ^ k) m \/ m == (S ^ k) n
Proof.n, m:t
exists k : nat, n == (S ^ k) m \/ m == (S ^ k) n
revert n.m:t
forall n : t,
exists k : nat, n == (S ^ k) m \/ m == (S ^ k) n
apply central_induction with (z:=m).m:t
Proper (eq ==> iff)
  (fun n : t =>
   exists k : nat,
     n ==
     nat_rect (fun _ : nat => t) m (fun _ : nat => S)
       k \/
     m ==
     nat_rect (fun _ : nat => t) n (fun _ : nat => S)
       k)
m:t
exists k : nat,
  m ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
  m ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
m:t
forall n : t,
(exists k : nat,
   n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) n (fun _ : nat => S) k) <->
(exists k : nat,
   S n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) (S n)
     (fun _ : nat => S) k)
 {m:t
Proper (eq ==> iff)
  (fun n : t =>
   exists k : nat,
     n ==
     nat_rect (fun _ : nat => t) m (fun _ : nat => S)
       k \/
     m ==
     nat_rect (fun _ : nat => t) n (fun _ : nat => S)
       k) intros x y eq_xy; apply ex_iff_morphism.m, x, y:t
eq_xy:x == y
pointwise_relation nat iff
  (fun k : nat =>
   x ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) x (fun _ : nat => S) k)
  (fun k : nat =>
   y ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) y (fun _ : nat => S) k)
  intros n; apply or_iff_morphism.m, x, y:t
eq_xy:x == y
n:nat
x ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) n <->
y ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) n
m, x, y:t
eq_xy:x == y
n:nat
m ==
nat_rect (fun _ : nat => t) x (fun _ : nat => S) n <->
m ==
nat_rect (fun _ : nat => t) y (fun _ : nat => S) n
 +m, x, y:t
eq_xy:x == y
n:nat
x ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) n <->
y ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) n split; intros; etransitivity; try eassumption; now symmetry.
 +m, x, y:t
eq_xy:x == y
n:nat
m ==
nat_rect (fun _ : nat => t) x (fun _ : nat => S) n <->
m ==
nat_rect (fun _ : nat => t) y (fun _ : nat => S) n split; intros; (etransitivity; [eassumption|]); [|symmetry];
    (eapply nat_rect_wd; [eassumption|apply succ_wd]).
 }m:t
exists k : nat,
  m ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
  m ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
m:t
forall n : t,
(exists k : nat,
   n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) n (fun _ : nat => S) k) <->
(exists k : nat,
   S n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) (S n)
     (fun _ : nat => S) k)
exists 0%nat.m:t
m ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 0 \/
m ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 0
m:t
forall n : t,
(exists k : nat,
   n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) n (fun _ : nat => S) k) <->
(exists k : nat,
   S n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) (S n)
     (fun _ : nat => S) k) now left.m:t
forall n : t,
(exists k : nat,
   n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) n (fun _ : nat => S) k) <->
(exists k : nat,
   S n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) (S n)
     (fun _ : nat => S) k)
intros n.m, n:t
(exists k : nat,
   n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) n (fun _ : nat => S) k) <->
(exists k : nat,
   S n ==
   nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
   m ==
   nat_rect (fun _ : nat => t) (S n)
     (fun _ : nat => S) k) split; intros [k [L|R]].m, n:t
k:nat
L:n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
exists (Datatypes.S k).m, n:t
k:nat
L:n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S k) \/
m ==
nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
  (Datatypes.S k)
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 left.m, n:t
k:nat
L:n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S k)
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 now apply succ_wd.m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
destruct k as [|k].m, n:t
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) 0
exists k : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S)
  (Datatypes.S k)
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
simpl in R.m, n:t
R:m == n
exists k : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S)
  (Datatypes.S k)
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 exists 1%nat.m, n:t
R:m == n
S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 1 \/
m ==
nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S) 1
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S)
  (Datatypes.S k)
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 left.m, n:t
R:m == n
S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 1
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S)
  (Datatypes.S k)
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 now apply succ_wd.m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S)
  (Datatypes.S k)
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
rewrite nat_rect_succ_r in R.m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  S n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S)
    k0
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 exists k.m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
m ==
nat_rect (fun _ : nat => t) (S n) (fun _ : nat => S) k
m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 now right.m, n:t
k:nat
L:S n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
destruct k as [|k]; simpl in L.m, n:t
L:S n == m
exists k : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
m, n:t
k:nat
L:S n ==
S
  (nat_rect (fun _ : nat => t) m
     (fun _ : nat => S) k)
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
exists 1%nat.m, n:t
L:S n == m
n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 1 \/
m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) 1
m, n:t
k:nat
L:S n ==
S
  (nat_rect (fun _ : nat => t) m
     (fun _ : nat => S) k)
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 now right.m, n:t
k:nat
L:S n ==
S
  (nat_rect (fun _ : nat => t) m
     (fun _ : nat => S) k)
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
apply succ_inj in L.m, n:t
k:nat
L:n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 exists k.m, n:t
k:nat
L:n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k \/
m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0 now left.m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  m ==
  nat_rect (fun _ : nat => t) n (fun _ : nat => S) k0
exists (Datatypes.S k).m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S k) \/
m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S)
  (Datatypes.S k) right.m, n:t
k:nat
R:m ==
nat_rect (fun _ : nat => t) (S n)
  (fun _ : nat => S) k
m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S)
  (Datatypes.S k) now rewrite nat_rect_succ_r.
Qed.

Generalized version of pred_succ when iterating

Lemma succ_swap_pred : forall k n m, n == (S^k) m -> m == (P^k) n.forall (k : nat) (n m : t),
n == (S ^ k) m -> m == (P ^ k) n
Proof.forall (k : nat) (n m : t),
n == (S ^ k) m -> m == (P ^ k) n
induction k.forall n m : t,
n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 0 ->
m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => P) 0
k:nat
IHk:forall n m : t,
n == nat_rect (fun _ : nat => t) m (fun _ : nat => S) k ->
m == nat_rect (fun _ : nat => t) n (fun _ : nat => P) k
forall n m : t,
n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S k) ->
m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => P)
  (Datatypes.S k)
simpl; auto with *.k:nat
IHk:forall n m : t,
n == nat_rect (fun _ : nat => t) m (fun _ : nat => S) k ->
m == nat_rect (fun _ : nat => t) n (fun _ : nat => P) k
forall n m : t,
n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S k) ->
m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => P)
  (Datatypes.S k)
simpl; intros.k:nat
IHk:forall n0 m0 : t,
n0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) k ->
m0 == nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k
n, m:t
H:n ==
S
  (nat_rect (fun _ : nat => t) m
     (fun _ : nat => S) k)
m ==
P (nat_rect (fun _ : nat => t) n (fun _ : nat => P) k) apply pred_wd in H.k:nat
IHk:forall n0 m0 : t,
n0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) k ->
m0 == nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k
n, m:t
H:P n ==
P
  (S
     (nat_rect (fun _ : nat => t) m
        (fun _ : nat => S) k))
m ==
P (nat_rect (fun _ : nat => t) n (fun _ : nat => P) k) rewrite pred_succ in H.k:nat
IHk:forall n0 m0 : t,
n0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) k ->
m0 == nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k
n, m:t
H:P n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
m ==
P (nat_rect (fun _ : nat => t) n (fun _ : nat => P) k) apply IHk in H; auto.k:nat
IHk:forall n0 m0 : t,
n0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) k ->
m0 == nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k
n, m:t
H:m ==
nat_rect (fun _ : nat => t) (P n)
  (fun _ : nat => P) k
m ==
P (nat_rect (fun _ : nat => t) n (fun _ : nat => P) k)
rewrite <- nat_rect_succ_r in H; auto.
Qed.

From a given point, all others are iterated successors or iterated predecessors.

Lemma itersucc_or_iterpred : forall n m, exists k, n == (S^k) m \/ n == (P^k) m.forall n m : t,
exists k : nat, n == (S ^ k) m \/ n == (P ^ k) m
Proof.forall n m : t,
exists k : nat, n == (S ^ k) m \/ n == (P ^ k) m
intros n m.n, m:t
exists k : nat, n == (S ^ k) m \/ n == (P ^ k) m destruct (itersucc_or_itersucc n m) as (k,[H|H]).n, m:t
k:nat
H:n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => P) k0
n, m:t
k:nat
H:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => P) k0
exists k; left; auto.n, m:t
k:nat
H:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
exists k0 : nat,
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => S) k0 \/
  n ==
  nat_rect (fun _ : nat => t) m (fun _ : nat => P) k0
exists k; right.n, m:t
k:nat
H:m ==
nat_rect (fun _ : nat => t) n (fun _ : nat => S) k
n ==
nat_rect (fun _ : nat => t) m (fun _ : nat => P) k apply succ_swap_pred; auto.
Qed.

In particular, all points are either iterated successors of 0 or iterated predecessors of 0 (or both).

Lemma itersucc0_or_iterpred0 :
 forall n, exists p:nat, n == (S^p) 0 \/ n == (P^p) 0.forall n : t,
exists p : nat, n == (S ^ p) 0 \/ n == (P ^ p) 0
Proof.forall n : t,
exists p : nat, n == (S ^ p) 0 \/ n == (P ^ p) 0
 intros n.n:t
exists p : nat, n == (S ^ p) 0 \/ n == (P ^ p) 0 exact (itersucc_or_iterpred n 0).
Qed.

Study of initial point w.r.t. succ (if any).

Definition initial n := forall m, n ~= S m.

Lemma initial_alt : forall n, initial n <-> S (P n) ~= n.forall n : t, initial n <-> S (P n) ~= n
Proof.forall n : t, initial n <-> S (P n) ~= n
split.n:t
initial n -> S (P n) ~= n
n:t
S (P n) ~= n -> initial n intros Bn EQ.n:t
Bn:initial n
EQ:S (P n) == n
False
n:t
S (P n) ~= n -> initial n symmetry in EQ.n:t
Bn:initial n
EQ:n == S (P n)
False
n:t
S (P n) ~= n -> initial n destruct (Bn _ EQ).n:t
S (P n) ~= n -> initial n
intros NEQ m EQ.n:t
NEQ:S (P n) ~= n
m:t
EQ:n == S m
False apply NEQ.n:t
NEQ:S (P n) ~= n
m:t
EQ:n == S m
S (P n) == n rewrite EQ, pred_succ; auto with *.
Qed.

Lemma initial_alt2 : forall n, initial n <-> ~exists m, n == S m.forall n : t, initial n <-> ~ (exists m : t, n == S m)
Proof.forall n : t, initial n <-> ~ (exists m : t, n == S m) firstorder. Qed.

First case: let's assume such an initial point exists (i.e. S isn't surjective)...

Section InitialExists.
Hypothesis init : t.
Hypothesis Initial : initial init.

... then we have unicity of this initial point.

Lemma initial_unique : forall m, initial m -> m == init.init:t
Initial:initial init
forall m : t, initial m -> m == init
Proof.init:t
Initial:initial init
forall m : t, initial m -> m == init
intros m Im.init:t
Initial:initial init
m:t
Im:initial m
m == init destruct (itersucc_or_itersucc init m) as (p,[H|H]).init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:init ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) p
m == init
init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
m == init
destruct p.init:t
Initial:initial init
m:t
Im:initial m
H:init ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 0
m == init
init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:init ==
nat_rect (fun _ : nat => t) m 
  (fun _ : nat => S) (Datatypes.S p)
m == init
init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
m == init now simpl in *.init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:init ==
nat_rect (fun _ : nat => t) m 
  (fun _ : nat => S) (Datatypes.S p)
m == init
init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
m == init destruct (Initial _ H).init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
m == init
destruct p.init:t
Initial:initial init
m:t
Im:initial m
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) 0
m == init
init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) (Datatypes.S p)
m == init now simpl in *.init:t
Initial:initial init
m:t
Im:initial m
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) (Datatypes.S p)
m == init destruct (Im _ H).
Qed.

... then all other points are descendant of it.

Lemma initial_ancestor : forall m, exists p, m == (S^p) init.init:t
Initial:initial init
forall m : t, exists p : nat, m == (S ^ p) init
Proof.init:t
Initial:initial init
forall m : t, exists p : nat, m == (S ^ p) init
intros m.init:t
Initial:initial init
m:t
exists p : nat, m == (S ^ p) init destruct (itersucc_or_itersucc init m) as (p,[H|H]).init:t
Initial:initial init
m:t
p:nat
H:init ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) p
exists p0 : nat,
  m ==
  nat_rect (fun _ : nat => t) init (fun _ : nat => S)
    p0
init:t
Initial:initial init
m:t
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
exists p0 : nat,
  m ==
  nat_rect (fun _ : nat => t) init 
    (fun _ : nat => S) p0
destruct p; simpl in *; auto.init:t
Initial:initial init
m:t
H:init == m
exists p : nat,
  m ==
  nat_rect (fun _ : nat => t) init (fun _ : nat => S)
    p
init:t
Initial:initial init
m:t
p:nat
H:init ==
S
  (nat_rect (fun _ : nat => t) m
     (fun _ : nat => S) p)
exists p0 : nat,
  m ==
  nat_rect (fun _ : nat => t) init 
    (fun _ : nat => S) p0
init:t
Initial:initial init
m:t
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
exists p0 : nat,
  m ==
  nat_rect (fun _ : nat => t) init 
    (fun _ : nat => S) p0 exists O; auto with *.init:t
Initial:initial init
m:t
p:nat
H:init ==
S
  (nat_rect (fun _ : nat => t) m
     (fun _ : nat => S) p)
exists p0 : nat,
  m ==
  nat_rect (fun _ : nat => t) init (fun _ : nat => S)
    p0
init:t
Initial:initial init
m:t
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
exists p0 : nat,
  m ==
  nat_rect (fun _ : nat => t) init 
    (fun _ : nat => S) p0 destruct (Initial _ H).init:t
Initial:initial init
m:t
p:nat
H:m ==
nat_rect (fun _ : nat => t) init
  (fun _ : nat => S) p
exists p0 : nat,
  m ==
  nat_rect (fun _ : nat => t) init (fun _ : nat => S)
    p0
exists p; auto.
Qed.

NB : We would like to have pred n == n for the initial element, but nothing forces that. For instance we can have -3 as initial point, and P(-3) = 2. A bit odd indeed, but legal according to NZDomainSig. We can hence have n == (P^k) m without ∃ k', m == (S^k') n.

We need decidability of eq (or classical reasoning) for this:

Section SuccPred.
Hypothesis eq_decidable : forall n m, n==m \/ n~=m.
Lemma succ_pred_approx : forall n, ~initial n -> S (P n) == n.init:t
Initial:initial init
eq_decidable:forall n m : t, n == m \/ n ~= m
forall n : t, ~ initial n -> S (P n) == n
Proof.init:t
Initial:initial init
eq_decidable:forall n m : t, n == m \/ n ~= m
forall n : t, ~ initial n -> S (P n) == n
intros n NB.init:t
Initial:initial init
eq_decidable:forall n0 m : t, n0 == m \/ n0 ~= m
n:t
NB:~ initial n
S (P n) == n rewrite initial_alt in NB.init:t
Initial:initial init
eq_decidable:forall n0 m : t, n0 == m \/ n0 ~= m
n:t
NB:~ S (P n) ~= n
S (P n) == n
destruct (eq_decidable (S (P n)) n); auto.init:t
Initial:initial init
eq_decidable:forall n0 m : t, n0 == m \/ n0 ~= m
n:t
NB:~ S (P n) ~= n
H:S (P n) ~= n
S (P n) == n
elim NB; auto.
Qed.
End SuccPred.
End InitialExists.

Second case : let's suppose now S surjective, i.e. no initial point.

Section InitialDontExists.

Hypothesis succ_onto : forall n, exists m, n == S m.

Lemma succ_onto_gives_succ_pred : forall n, S (P n) == n.succ_onto:forall n : t, exists m : t, n == S m
forall n : t, S (P n) == n
Proof.succ_onto:forall n : t, exists m : t, n == S m
forall n : t, S (P n) == n
intros n.succ_onto:forall n0 : t, exists m : t, n0 == S m
n:t
S (P n) == n destruct (succ_onto n) as (m,H).succ_onto:forall n0 : t, exists m0 : t, n0 == S m0
n, m:t
H:n == S m
S (P n) == n rewrite H, pred_succ; auto with *.
Qed.

Lemma succ_onto_pred_injective : forall n m, P n == P m -> n == m.succ_onto:forall n : t, exists m : t, n == S m
forall n m : t, P n == P m -> n == m
Proof.succ_onto:forall n : t, exists m : t, n == S m
forall n m : t, P n == P m -> n == m
intros n m.succ_onto:forall n0 : t, exists m0 : t, n0 == S m0
n, m:t
P n == P m -> n == m intros H; apply succ_wd in H.succ_onto:forall n0 : t, exists m0 : t, n0 == S m0
n, m:t
H:S (P n) == S (P m)
n == m
rewrite !succ_onto_gives_succ_pred in H; auto.
Qed.

End InitialDontExists.

To summarize:

S is always injective, P is always surjective (thanks to pred_succ).

I) If S is not surjective, we have an initial point, which is unique. This bottom is below zero: we have N shifted (or not) to the left. P cannot be injective: P init = P (S (P init)). (P init) can be arbitrary.

II) If S is surjective, we have ∀ n, S (P n) = n, S and P are bijective and reciprocal.

IIa) if ∃ k≠O, 0 == S^k 0, then we have a cyclic structure Z/nZ IIb) otherwise, we have Z

An alternative induction principle using S and P.

It is weaker than bi_induction. For instance it cannot prove that we can go from one point by many S or many P, but only by many S mixed with many P. Think of a model with two copies of N:

0, 1=S 0, 2=S 1, ... 0', 1'=S 0', 2'=S 1', ...

and P 0 = 0' and P 0' = 0.

Lemma bi_induction_pred :
  forall A : t -> Prop, Proper (eq==>iff) A ->
    A 0 -> (forall n, A n -> A (S n)) -> (forall n, A n -> A (P n)) ->
    forall n, A n.forall A : t -> Prop,
Proper (eq ==> iff) A ->
A 0 ->
(forall n : t, A n -> A (S n)) ->
(forall n : t, A n -> A (P n)) -> forall n : t, A n
Proof.forall A : t -> Prop,
Proper (eq ==> iff) A ->
A 0 ->
(forall n : t, A n -> A (S n)) ->
(forall n : t, A n -> A (P n)) -> forall n : t, A n
intros.A:t -> Prop
H:Proper (eq ==> iff) A
H0:A 0
H1:forall n0 : t, A n0 -> A (S n0)
H2:forall n0 : t, A n0 -> A (P n0)
n:t
A n apply bi_induction; auto.A:t -> Prop
H:Proper (eq ==> iff) A
H0:A 0
H1:forall n0 : t, A n0 -> A (S n0)
H2:forall n0 : t, A n0 -> A (P n0)
n:t
forall n0 : t, A n0 <-> A (S n0)
clear n.A:t -> Prop
H:Proper (eq ==> iff) A
H0:A 0
H1:forall n : t, A n -> A (S n)
H2:forall n : t, A n -> A (P n)
forall n : t, A n <-> A (S n) intros n; split; auto.A:t -> Prop
H:Proper (eq ==> iff) A
H0:A 0
H1:forall n0 : t, A n0 -> A (S n0)
H2:forall n0 : t, A n0 -> A (P n0)
n:t
A (S n) -> A n
intros G; apply H2 in G.A:t -> Prop
H:Proper (eq ==> iff) A
H0:A 0
H1:forall n0 : t, A n0 -> A (S n0)
H2:forall n0 : t, A n0 -> A (P n0)
n:t
G:A (P (S n))
A n rewrite pred_succ in G; auto.
Qed.

Lemma central_induction_pred :
  forall A : t -> Prop, Proper (eq==>iff) A -> forall n0,
    A n0 -> (forall n, A n -> A (S n)) -> (forall n, A n -> A (P n)) ->
    forall n, A n.forall A : t -> Prop,
Proper (eq ==> iff) A ->
forall n0 : t,
A n0 ->
(forall n : t, A n -> A (S n)) ->
(forall n : t, A n -> A (P n)) -> forall n : t, A n
Proof.forall A : t -> Prop,
Proper (eq ==> iff) A ->
forall n0 : t,
A n0 ->
(forall n : t, A n -> A (S n)) ->
(forall n : t, A n -> A (P n)) -> forall n : t, A n
intros.A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
A n
assert (A 0).A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
A 0
A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
H3:A 0
A n
destruct (itersucc_or_iterpred 0 n0) as (k,[Hk|Hk]); rewrite Hk; clear Hk.A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
k:nat
A
  (nat_rect (fun _ : nat => t) n0 (fun _ : nat => S) k)
A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
k:nat
A
  (nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k)
A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
H3:A 0
A n
 clear H2.A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
n:t
k:nat
A
  (nat_rect (fun _ : nat => t) n0 (fun _ : nat => S) k)
A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
k:nat
A
  (nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k)
A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
H3:A 0
A n induction k; simpl in *; auto.A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
k:nat
A
  (nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k)
A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
H3:A 0
A n
 clear H1.A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H2:forall n1 : t, A n1 -> A (P n1)
n:t
k:nat
A
  (nat_rect (fun _ : nat => t) n0 (fun _ : nat => P) k)
A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
H3:A 0
A n induction k; simpl in *; auto.A:t -> Prop
H:Proper (eq ==> iff) A
n0:t
H0:A n0
H1:forall n1 : t, A n1 -> A (S n1)
H2:forall n1 : t, A n1 -> A (P n1)
n:t
H3:A 0
A n
apply bi_induction_pred; auto.
Qed.

End NZDomainProp.

We now focus on the translation from nat into NZ. First, relationship with 0, succ, pred.

Module NZOfNat (Import NZ:NZDomainSig').

Definition ofnat (n : nat) : t := (S^n) 0.

Declare Scope ofnat.
Local Open Scope ofnat.
Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.

Lemma ofnat_zero : [O] == 0.[0] == 0
Proof.[0] == 0
reflexivity.
Qed.

Lemma ofnat_succ : forall n, [Datatypes.S n] == succ [n].forall n : nat, [Datatypes.S n] == S [n]
Proof.forall n : nat, [Datatypes.S n] == S [n]
 now unfold ofnat.
Qed.

Lemma ofnat_pred : forall n, n<>O -> [Peano.pred n] == P [n].forall n : nat, n <> 0 -> [Nat.pred n] == P [n]
Proof.forall n : nat, n <> 0 -> [Nat.pred n] == P [n]
 unfold ofnat.forall n : nat,
n <> 0 ->
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
  (Nat.pred n) ==
P (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S) n) destruct n.0 <> 0 ->
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
  (Nat.pred 0) ==
P (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S) 0)
n:nat
Datatypes.S n <> 0 ->
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
  (Nat.pred (Datatypes.S n)) ==
P
  (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
     (Datatypes.S n)) destruct 1; auto.n:nat
Datatypes.S n <> 0 ->
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
  (Nat.pred (Datatypes.S n)) ==
P
  (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
     (Datatypes.S n))
 intros _.n:nat
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
  (Nat.pred (Datatypes.S n)) ==
P
  (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
     (Datatypes.S n)) simpl.n:nat
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S) n ==
P
  (S
     (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
        n)) symmetry.n:nat
P
  (S
     (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
        n)) ==
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S) n apply pred_succ.
Qed.

Since P 0 can be anything in NZ (either -1, 0, or even other numbers, we cannot state previous lemma for n=O.

End NZOfNat.

If we require in addition a strict order on NZ, we can prove that ofnat is injective, and hence that NZ is infinite (i.e. we ban Z/nZ models)

Module NZOfNatOrd (Import NZ:NZOrdSig').
Include NZOfNat NZ.
Include NZBaseProp NZ <+ NZOrderProp NZ.
Local Open Scope ofnat.

Theorem ofnat_S_gt_0 :
  forall n : nat, 0 < [Datatypes.S n].forall n : nat, 0 < [Datatypes.S n]
Proof.forall n : nat, 0 < [Datatypes.S n]
unfold ofnat.forall n : nat,
0 <
nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
  (Datatypes.S n)
intros n; induction n as [| n IH]; simpl in *.0 < S 0
n:nat
IH:0 <
S
  (nat_rect (fun _ : nat => t) 0
     (fun _ : nat => S) n)
0 <
S
  (S
     (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
        n))
apply lt_succ_diag_r.n:nat
IH:0 <
S
  (nat_rect (fun _ : nat => t) 0
     (fun _ : nat => S) n)
0 <
S
  (S
     (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
        n))
apply lt_trans with (S 0).n:nat
IH:0 <
S
  (nat_rect (fun _ : nat => t) 0
     (fun _ : nat => S) n)
0 < S 0
n:nat
IH:0 <
S
  (nat_rect (fun _ : nat => t) 0
     (fun _ : nat => S) n)
S 0 <
S
  (S
     (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
        n)) apply lt_succ_diag_r.n:nat
IH:0 <
S
  (nat_rect (fun _ : nat => t) 0
     (fun _ : nat => S) n)
S 0 <
S
  (S
     (nat_rect (fun _ : nat => t) 0 (fun _ : nat => S)
        n)) now rewrite <- succ_lt_mono.
Qed.

Theorem ofnat_S_neq_0 :
  forall n : nat, 0 ~= [Datatypes.S n].forall n : nat, 0 ~= [Datatypes.S n]
Proof.forall n : nat, 0 ~= [Datatypes.S n]
intros.n:nat
0 ~= [Datatypes.S n] apply lt_neq, ofnat_S_gt_0.
Qed.

Lemma ofnat_injective : forall n m, [n]==[m] -> n = m.forall n m : nat, [n] == [m] -> n = m
Proof.forall n m : nat, [n] == [m] -> n = m
induction n as [|n IH]; destruct m; auto.m:nat
[0] == [Datatypes.S m] -> 0 = Datatypes.S m
n:nat
IH:forall m : nat, [n] == [m] -> n = m
[Datatypes.S n] == [0] -> Datatypes.S n = 0
n:nat
IH:forall m0 : nat, [n] == [m0] -> n = m0
m:nat
[Datatypes.S n] == [Datatypes.S m] ->
Datatypes.S n = Datatypes.S m
intros H; elim (ofnat_S_neq_0 _ H).n:nat
IH:forall m : nat, [n] == [m] -> n = m
[Datatypes.S n] == [0] -> Datatypes.S n = 0
n:nat
IH:forall m0 : nat, [n] == [m0] -> n = m0
m:nat
[Datatypes.S n] == [Datatypes.S m] ->
Datatypes.S n = Datatypes.S m
intros H; symmetry in H; elim (ofnat_S_neq_0 _ H).n:nat
IH:forall m0 : nat, [n] == [m0] -> n = m0
m:nat
[Datatypes.S n] == [Datatypes.S m] ->
Datatypes.S n = Datatypes.S m
intros.n:nat
IH:forall m0 : nat, [n] == [m0] -> n = m0
m:nat
H:[Datatypes.S n] == [Datatypes.S m]
Datatypes.S n = Datatypes.S m f_equal.n:nat
IH:forall m0 : nat, [n] == [m0] -> n = m0
m:nat
H:[Datatypes.S n] == [Datatypes.S m]
n = m apply IH.n:nat
IH:forall m0 : nat, [n] == [m0] -> n = m0
m:nat
H:[Datatypes.S n] == [Datatypes.S m]
[n] == [m] now rewrite <- succ_inj_wd.
Qed.

Lemma ofnat_eq : forall n m, [n]==[m] <-> n = m.forall n m : nat, [n] == [m] <-> n = m
Proof.forall n m : nat, [n] == [m] <-> n = m
split.n, m:nat
[n] == [m] -> n = m
n, m:nat
n = m -> [n] == [m] apply ofnat_injective.n, m:nat
n = m -> [n] == [m] intros; now subst.
Qed.

(* In addition, we can prove that [ofnat] preserves order. *)

Lemma ofnat_lt : forall n m : nat, [n]<[m] <-> (n<m)%nat.forall n m : nat, [n] < [m] <-> n < m
Proof.forall n m : nat, [n] < [m] <-> n < m
induction n as [|n IH]; destruct m; repeat rewrite ofnat_zero; split.0 < 0 -> 0 < 0
0 < 0 -> 0 < 0
m:nat
0 < [Datatypes.S m] -> 0 < Datatypes.S m
m:nat
0 < Datatypes.S m -> 0 < [Datatypes.S m]
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
[Datatypes.S n] < 0 -> Datatypes.S n < 0
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
Datatypes.S n < 0 -> [Datatypes.S n] < 0
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
[Datatypes.S n] < [Datatypes.S m] ->
Datatypes.S n < Datatypes.S m
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
intro H; elim (lt_irrefl _ H).0 < 0 -> 0 < 0
m:nat
0 < [Datatypes.S m] -> 0 < Datatypes.S m
m:nat
0 < Datatypes.S m -> 0 < [Datatypes.S m]
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
[Datatypes.S n] < 0 -> Datatypes.S n < 0
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
Datatypes.S n < 0 -> [Datatypes.S n] < 0
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
[Datatypes.S n] < [Datatypes.S m] ->
Datatypes.S n < Datatypes.S m
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
inversion 1.m:nat
0 < [Datatypes.S m] -> 0 < Datatypes.S m
m:nat
0 < Datatypes.S m -> 0 < [Datatypes.S m]
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
[Datatypes.S n] < 0 -> Datatypes.S n < 0
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
Datatypes.S n < 0 -> [Datatypes.S n] < 0
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
[Datatypes.S n] < [Datatypes.S m] ->
Datatypes.S n < Datatypes.S m
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
auto with arith.m:nat
0 < Datatypes.S m -> 0 < [Datatypes.S m]
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
[Datatypes.S n] < 0 -> Datatypes.S n < 0
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
Datatypes.S n < 0 -> [Datatypes.S n] < 0
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
[Datatypes.S n] < [Datatypes.S m] ->
Datatypes.S n < Datatypes.S m
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
intros; apply ofnat_S_gt_0.n:nat
IH:forall m : nat, [n] < [m] <-> n < m
[Datatypes.S n] < 0 -> Datatypes.S n < 0
n:nat
IH:forall m : nat, [n] < [m] <-> n < m
Datatypes.S n < 0 -> [Datatypes.S n] < 0
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
[Datatypes.S n] < [Datatypes.S m] ->
Datatypes.S n < Datatypes.S m
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
intro H; elim (lt_asymm _ _ H); apply ofnat_S_gt_0.n:nat
IH:forall m : nat, [n] < [m] <-> n < m
Datatypes.S n < 0 -> [Datatypes.S n] < 0
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
[Datatypes.S n] < [Datatypes.S m] ->
Datatypes.S n < Datatypes.S m
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
inversion 1.n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
[Datatypes.S n] < [Datatypes.S m] ->
Datatypes.S n < Datatypes.S m
n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
rewrite !ofnat_succ, <- succ_lt_mono, IH; auto with arith.n:nat
IH:forall m0 : nat, [n] < [m0] <-> n < m0
m:nat
Datatypes.S n < Datatypes.S m ->
[Datatypes.S n] < [Datatypes.S m]
rewrite !ofnat_succ, <- succ_lt_mono, IH; auto with arith.
Qed.

Lemma ofnat_le : forall n m : nat, [n]<=[m] <-> (n<=m)%nat.forall n m : nat, [n] <= [m] <-> n <= m
Proof.forall n m : nat, [n] <= [m] <-> n <= m
intros.n, m:nat
[n] <= [m] <-> n <= m rewrite lt_eq_cases, ofnat_lt, ofnat_eq.n, m:nat
n < m \/ n = m <-> n <= m
split.n, m:nat
n < m \/ n = m -> n <= m
n, m:nat
n <= m -> n < m \/ n = m
destruct 1; subst; auto with arith.n, m:nat
n <= m -> n < m \/ n = m
apply Lt.le_lt_or_eq.
Qed.

End NZOfNatOrd.

For basic operations, we can prove correspondence with their counterpart in nat.

Module NZOfNatOps (Import NZ:NZAxiomsSig').
Include NZOfNat NZ.
Local Open Scope ofnat.

Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m.forall (n : nat) (m : t), [n] + m == (S ^ n) m
Proof.forall (n : nat) (m : t), [n] + m == (S ^ n) m
 induction n; intros.m:t
[0] + m ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S) 0
n:nat
IHn:forall m0 : t,
[n] + m0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) n
m:t
[Datatypes.S n] + m ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S n)
 apply add_0_l.n:nat
IHn:forall m0 : t,
[n] + m0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) n
m:t
[Datatypes.S n] + m ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S n)
 rewrite ofnat_succ, add_succ_l.n:nat
IHn:forall m0 : t,
[n] + m0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) n
m:t
S ([n] + m) ==
nat_rect (fun _ : nat => t) m (fun _ : nat => S)
  (Datatypes.S n) simpl.n:nat
IHn:forall m0 : t,
[n] + m0 == nat_rect (fun _ : nat => t) m0 (fun _ : nat => S) n
m:t
S ([n] + m) ==
S (nat_rect (fun _ : nat => t) m (fun _ : nat => S) n) now f_equiv.
Qed.

Lemma ofnat_add : forall n m, [n+m] == [n]+[m].forall n m : nat, [n + m] == [n] + [m]
Proof.forall n m : nat, [n + m] == [n] + [m]
 intros.n, m:nat
[n + m] == [n] + [m] rewrite ofnat_add_l.n, m:nat
[n + m] ==
nat_rect (fun _ : nat => t) [m] (fun _ : nat => S) n
 induction n; simpl.m:nat
[m] == [m]
n, m:nat
IHn:[n + m] == nat_rect (fun _ : nat => t) [m] (fun _ : nat => S) n
S [n + m] ==
S
  (nat_rect (fun _ : nat => t) [m] (fun _ : nat => S)
     n) reflexivity.n, m:nat
IHn:[n + m] == nat_rect (fun _ : nat => t) [m] (fun _ : nat => S) n
S [n + m] ==
S
  (nat_rect (fun _ : nat => t) [m] (fun _ : nat => S)
     n)
 now f_equiv.
Qed.

Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].forall n m : nat, [n * m] == [n] * [m]
Proof.forall n m : nat, [n * m] == [n] * [m]
 induction n; simpl; intros.m:nat
0 == 0 * [m]
n:nat
IHn:forall m0 : nat, [n * m0] == [n] * [m0]
m:nat
[m + n * m] == S [n] * [m]
 symmetry.m:nat
0 * [m] == 0
n:nat
IHn:forall m0 : nat, [n * m0] == [n] * [m0]
m:nat
[m + n * m] == S [n] * [m] apply mul_0_l.n:nat
IHn:forall m0 : nat, [n * m0] == [n] * [m0]
m:nat
[m + n * m] == S [n] * [m]
 rewrite plus_comm.n:nat
IHn:forall m0 : nat, [n * m0] == [n] * [m0]
m:nat
[n * m + m] == S [n] * [m]
 rewrite ofnat_add, mul_succ_l.n:nat
IHn:forall m0 : nat, [n * m0] == [n] * [m0]
m:nat
[n * m] + [m] == [n] * [m] + [m]
 now f_equiv.
Qed.

Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.forall (n : t) (m : nat), n - [m] == (P ^ m) n
Proof.forall (n : t) (m : nat), n - [m] == (P ^ m) n
 induction m; simpl; intros.n:t
n - 0 == n
n:t
m:nat
IHm:n - [m] == nat_rect (fun _ : nat => t) n (fun _ : nat => P) m
n - S [m] ==
P (nat_rect (fun _ : nat => t) n (fun _ : nat => P) m)
 apply sub_0_r.n:t
m:nat
IHm:n - [m] == nat_rect (fun _ : nat => t) n (fun _ : nat => P) m
n - S [m] ==
P (nat_rect (fun _ : nat => t) n (fun _ : nat => P) m)
 rewrite sub_succ_r.n:t
m:nat
IHm:n - [m] == nat_rect (fun _ : nat => t) n (fun _ : nat => P) m
P (n - [m]) ==
P (nat_rect (fun _ : nat => t) n (fun _ : nat => P) m) now f_equiv.
Qed.

Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].forall n m : nat, m <= n -> [n - m] == [n] - [m]
Proof.forall n m : nat, m <= n -> [n - m] == [n] - [m]
 intros n m H.n, m:nat
H:m <= n
[n - m] == [n] - [m] rewrite ofnat_sub_r.n, m:nat
H:m <= n
[n - m] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m
 revert n H.m:nat
forall n : nat,
m <= n ->
[n - m] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m induction m.forall n : nat,
0 <= n ->
[n - 0] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) 0
m:nat
IHm:forall n : nat,
m <= n -> [n - m] == nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m
forall n : nat,
Datatypes.S m <= n ->
[n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P)
  (Datatypes.S m) intros.n:nat
H:0 <= n
[n - 0] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) 0
m:nat
IHm:forall n : nat,
m <= n -> [n - m] == nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m
forall n : nat,
Datatypes.S m <= n ->
[n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P)
  (Datatypes.S m)
 rewrite <- minus_n_O.n:nat
H:0 <= n
[n] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) 0
m:nat
IHm:forall n : nat,
m <= n -> [n - m] == nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m
forall n : nat,
Datatypes.S m <= n ->
[n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P)
  (Datatypes.S m) now simpl.m:nat
IHm:forall n : nat,
m <= n -> [n - m] == nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m
forall n : nat,
Datatypes.S m <= n ->
[n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P)
  (Datatypes.S m)
 intros.m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= n
[n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P)
  (Datatypes.S m)
 destruct n.m:nat
IHm:forall n : nat,
m <= n -> [n - m] == nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m
H:Datatypes.S m <= 0
[0 - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [0] (fun _ : nat => P)
  (Datatypes.S m)
m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
[Datatypes.S n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [Datatypes.S n]
  (fun _ : nat => P) (Datatypes.S m)
 inversion H.m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
[Datatypes.S n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) [Datatypes.S n]
  (fun _ : nat => P) (Datatypes.S m)
 rewrite nat_rect_succ_r.m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
[Datatypes.S n - Datatypes.S m] ==
nat_rect (fun _ : nat => t) (P [Datatypes.S n])
  (fun _ : nat => P) m
 simpl.m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
[n - m] ==
nat_rect (fun _ : nat => t) (P (S [n]))
  (fun _ : nat => P) m
 etransitivity.m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
[n - m] == ?y
m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
?y ==
nat_rect (fun _ : nat => t) (P (S [n]))
  (fun _ : nat => P) m apply IHm.m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
m <= n
m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m ==
nat_rect (fun _ : nat => t) (P (S [n]))
  (fun _ : nat => P) m auto with arith.m:nat
IHm:forall n0 : nat,
m <= n0 -> [n0 - m] == nat_rect (fun _ : nat => t) [n0] (fun _ : nat => P) m
n:nat
H:Datatypes.S m <= Datatypes.S n
nat_rect (fun _ : nat => t) [n] (fun _ : nat => P) m ==
nat_rect (fun _ : nat => t) (P (S [n]))
  (fun _ : nat => P) m
    eapply nat_rect_wd; [symmetry;apply pred_succ|apply pred_wd].
Qed.

End NZOfNatOps.