Library Coq.Numbers.NatInt.NZBase



Require Import NZAxioms.

Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig).
Open Local Scope NatIntScope.

Theorem NZneq_sym : forall n m : NZ, n ~= m -> m ~= n.

Theorem NZE_stepl : forall x y z : NZ, x == y -> x == z -> z == y.

Declare Left Step NZE_stepl.
Declare Right Step (proj1 (proj2 NZeq_equiv)).

Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.


Theorem NZsucc_inj_wd : forall n1 n2 : NZ, S n1 == S n2 <-> n1 == n2.

Theorem NZsucc_inj_wd_neg : forall n m : NZ, S n ~= S m <-> n ~= m.


Section CentralInduction.

Variable A : predicate NZ.

Hypothesis A_wd : predicate_wd NZeq A.

Add Morphism A with signature NZeq ==> iff as A_morph.

Theorem NZcentral_induction :
  forall z : NZ, A z ->
    (forall n : NZ, A n <-> A (S n)) ->
      forall n : NZ, A n.

End CentralInduction.

Tactic Notation "NZinduct" ident(n) :=
  induction_maker n ltac:(apply NZinduction).

Tactic Notation "NZinduct" ident(n) constr(u) :=
  induction_maker n ltac:(apply NZcentral_induction with (z := u)).

End NZBasePropFunct.