(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms specs

Currently, 8 lemmas remains to tackle. One proof is done via a _very_
brute-force ugly approach. The all story for proving composition of
phi and phi_inv (and the other way around) is surprisingly long and
tricky. In both cases, comments are welcome, I may have missed an
easier road (?)

As a consequence of the above, we have a additional time-eager
file in the stdlib (about a minute to compile here). 



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10973 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions