Advice on the use of arithmetic books (based largely on comments from
Robert Krug, and repeated in ../arithmetic-5/README):

  SUMMARY: Power users should include arithmetic-5/top; new users
  should probably instead include arithmetic/top-with-meta.

  Details:

  If you are willing to use dmr (see :doc dmr) and tolerate
  sometimes-slower (but more complete) reasoning, use arithmetic-5.
  Robert is not aware of any rewriting loops.

  If you are willing tolerate sometimes-slower (but more complete)
  reasoning, but you want to avoid dmr, use arithmetic-4.  However, if
  you're willing to use arithmetic-4, consider using arithmetic-5
  instead -- it doesn't require much more use of dmr, and it's much
  more up-to-date.  You may encounter rewriting loops.

  Don't use arithmetic-3.  It's not as powerful as arithmetic-4
  (Robert doesn't know if it's faster), and it has more rewriting
  loops than arithmetic-4.

  Note that arithmetic-2 is totally obsolete.  We may stop
  distributing it.

  If you want fast, lightweight arithmetic, use
  arithmetic/top-with-meta.

============================================================

Please see Section 0 of ../arithmetic-5/README for information about
which arithmetic books to use.

Contents of this directory:

README			This file
abs.lisp		Theorems about absolute value
binomial.lisp		A proof of the binomial theorem
certify.lsp		(ld "certify.lsp") to certify books in this directory
equalities.lisp		Arithmetic equality rules
factorial.lisp		Theorems about the factorial function
idiv.lisp		Theorems about integer division and related functions
inequalities.lisp	Arithmetic inequality rules
rational-listp.lisp	Very short book about lists of rationals
rationals-with-axioms-proved.lisp	Supersedes rationals-with-axioms.lisp
sumlist.lisp		Theorems about sum of a list of numbers
top.lisp		Putting it all together
top-with-meta.lisp      Extension of top.lisp by the books in ../meta

Many people contributed to these books, especially

  Bishop Brock
  John Cowles
  Matt Kaufmann  
  Art Flatau
  Ruben Gamboa