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 NZadd := plus.
Definition NZsub := minus.
Definition NZmul := mult.
Theorem NZeq_equiv : equiv nat NZeq.
Add Relation 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 NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_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.