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)