Library Coq.Numbers.Natural.Peano.NPeano

Require Import Arith.
Require Import Min.
Require Import Max.
Require Import NSub.

Module NPeanoAxiomsMod <: NAxiomsSig.
Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
Module Export NZAxiomsMod <: NZAxiomsSig.

Definition NZ := nat.
Definition NZeq := (@eq nat).
Definition NZ0 := 0.
Definition NZsucc := S.
Definition NZpred := pred.
Definition NZsub := minus.
Definition NZmul := mult.

Theorem NZeq_equiv : equiv nat NZeq.
reflexivity proved by (proj1 NZeq_equiv)
symmetry proved by (proj2 (proj2 NZeq_equiv))
transitivity proved by (proj1 (proj2 NZeq_equiv))
as NZeq_rel.

Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.

Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.

Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.

Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.

Theorem NZinduction :
forall A : nat -> Prop, predicate_wd (@eq nat) A ->
A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.

Theorem NZpred_succ : forall n : nat, pred (S n) = n.

Theorem NZadd_0_l : forall n : nat, 0 + n = n.

Theorem NZadd_succ_l : forall n m : nat, (S n) + m = S (n + m).

Theorem NZsub_0_r : forall n : nat, n - 0 = n.

Theorem NZsub_succ_r : forall n m : nat, n - (S m) = pred (n - m).

Theorem NZmul_0_l : forall n : nat, 0 * n = 0.

Theorem NZmul_succ_l : forall n m : nat, S n * m = n * m + m.

End NZAxiomsMod.

Definition NZlt := lt.
Definition NZle := le.
Definition NZmin := min.
Definition NZmax := max.

Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.

Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.

Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.

Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.

Theorem NZlt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.

Theorem NZlt_irrefl : forall n : nat, ~ (n < n).

Theorem NZlt_succ_r : forall n m : nat, n < S m <-> n <= m.

Theorem NZmin_l : forall n m : nat, n <= m -> NZmin n m = n.

Theorem NZmin_r : forall n m : nat, m <= n -> NZmin n m = m.

Theorem NZmax_l : forall n m : nat, m <= n -> NZmax n m = n.

Theorem NZmax_r : forall n m : nat, n <= m -> NZmax n m = m.

End NZOrdAxiomsMod.

Definition recursion : forall A : Type, A -> (nat -> A -> A) -> nat -> A :=
fun A : Type => nat_rect (fun _ => A).
Implicit Arguments recursion [A].

Theorem succ_neq_0 : forall n : nat, S n <> 0.

Theorem pred_0 : pred 0 = 0.

Theorem recursion_wd : forall (A : Type) (Aeq : relation A),
forall a a' : A, Aeq a a' ->
forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' ->
forall n n' : nat, n = n' ->
Aeq (recursion a f n) (recursion a' f' n').

Theorem recursion_0 :
forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a.

Theorem recursion_succ :
forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A),
Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f ->
forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).

End NPeanoAxiomsMod.

Module Export NPeanoSubPropMod := NSubPropFunct NPeanoAxiomsMod.