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.