Attempt to prove a theorem using various arithmetic libraries

This book shows how one can use make-event to try different proof strategies for a given theorem, or more generally a given event, until one works. Specifically, the strategies employed in this example are the use of different built-in arithmetic books.

(encapsulate () (local (include-book <book>)) extra-event-1 ... extra-event-k event)

for an appropriate

The general form is:

(proof-by-arith event &optional quietp arith-book-alist)

where