Library Coq.Numbers.Integer.BigZ.BigZ
Require Export BigN.
Require Import ZMulOrder.
Require Import ZSig.
Require Import ZSigZAxioms.
Require Import ZMake.
Module BigZ <: ZType := ZMake.Make BigN.
Module BigZ implements ZAxiomsSig
Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod.
Notations about BigZ
Notation bigZ := BigZ.t.
Delimit Scope bigZ_scope with bigZ.
Notation Local "0" := BigZ.zero : bigZ_scope.
Infix "+" := BigZ.add : bigZ_scope.
Infix "-" := BigZ.sub : bigZ_scope.
Notation "- x" := (BigZ.opp x) : bigZ_scope.
Infix "*" := BigZ.mul : bigZ_scope.
Infix "/" := BigZ.div : bigZ_scope.
Infix "?=" := BigZ.compare : bigZ_scope.
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
Infix "<" := BigZ.lt : bigZ_scope.
Infix "<=" := BigZ.le : bigZ_scope.
Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
Open Scope bigZ_scope.
Some additional results about BigZ
Theorem spec_to_Z: forall n:bigZ,
BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
Theorem spec_to_N n:
([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
BigN.to_Z (BigZ.to_N n) = [n].
Lemma sub_opp : forall x y : bigZ, x - y == x + (- y).
Lemma add_opp : forall x : bigZ, x + (- x) == 0.
BigZ is a ring
Lemma BigZring :
ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
Add Ring BigZr : BigZring.
Todo: tactic translating from BigZ to Z + omega
Todo: micromega