# Library Coq.Numbers.Natural.Abstract.NAxioms

Require Export NZAxioms.
Module Type NAxioms (Import NZ : NZDomainSig').
Axiom pred_0 : P 0 == 0.
Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A.
Implicit Arguments recursion [A].
Declare Instance recursion_wd (A : Type) (Aeq : relation A) :
Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
Axiom recursion_0 :
forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a.
Axiom recursion_succ :
forall (A : Type) (Aeq : relation A) (a : A) (f : t -> A -> A),
Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)).
End NAxioms.
Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms.
Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms.