Library Coq.Numbers.Natural.BigN.BigN
Author: Arnaud Spiwack
Require Export Int31.
Require Import CyclicAxioms.
Require Import Cyclic31.
Require Import NSig.
Require Import NSigNAxioms.
Require Import NMake.
Require Import NSub.
Module BigN <: NType := NMake.Make Int31Cyclic.
Module BigN implements NAxiomsSig
Module Export BigNAxiomsMod := NSig_NAxioms BigN.
Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod.
Notations about BigN
Notation bigN := BigN.t.
Delimit Scope bigN_scope with bigN.
Notation Local "0" := BigN.zero : bigN_scope.
Infix "+" := BigN.add : bigN_scope.
Infix "-" := BigN.sub : bigN_scope.
Infix "*" := BigN.mul : bigN_scope.
Infix "/" := BigN.div : bigN_scope.
Infix "?=" := BigN.compare : bigN_scope.
Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
Infix "<" := BigN.lt : bigN_scope.
Infix "<=" := BigN.le : bigN_scope.
Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
Open Scope bigN_scope.
Example of reasoning about BigN
BigN is a semi-ring
Lemma BigNring :
semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
Add Ring BigNr : BigNring.
Todo: tactic translating from BigN to Z + omega
Todo: micromega