Library Coq.Numbers.Integer.Abstract.ZBase



Require Export Decidable.
Require Export ZAxioms.
Require Import NZMulOrder.

Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).


Open Local Scope IntScope.

Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod.

Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2.
Theorem Zpred_wd : forall n1 n2 : Z, n1 == n2 -> P n1 == P n2.
Theorem Zpred_succ : forall n : Z, P (S n) == n.
Theorem Zeq_refl : forall n : Z, n == n.
Theorem Zeq_sym : forall n m : Z, n == m -> m == n.
Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p.
Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n.
Theorem Zsucc_inj : forall n1 n2 : Z, S n1 == S n2 -> n1 == n2.
Theorem Zsucc_inj_wd : forall n1 n2 : Z, S n1 == S n2 <-> n1 == n2.
Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m.
Theorem Zeq_dec : forall n m : Z, decidable (n == m).
Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
Theorem Zcentral_induction :
forall A : Z -> Prop, predicate_wd Zeq A ->
  forall z : Z, A z ->
    (forall n : Z, A n <-> A (S n)) ->
      forall n : Z, A n.
Theorem Zpred_inj : forall n m : Z, P n == P m -> n == m.

Theorem Zpred_inj_wd : forall n1 n2 : Z, P n1 == P n2 <-> n1 == n2.

End ZBasePropFunct.