BigQ: an efficient implementation of rational numbers
Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007
We choose for BigQ an implemention with
multiple representation of 0: 0, 1/0, 2/0 etc.
See
QMake.v
First, we provide translations functions between
BigN and
BigZ
We can also reason by switching to QArith thanks to tactic
BigQ.qify.