Library Coq.Numbers.Integer.BigZ.BigZ
Module BigZ implements ZAxiomsSig
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
BigZ is a ring
Todo: tactic translating from BigZ to Z + omega
Todo: micromega