|
|
|---|
|
|
|
|---|
Definitions for congruence reasoning about integers/naturals/bits.
Note: to use this book at full strength, do:
(include-book "std/basic/arith-equivs" :dir :system) (local (in-theory (enable* arith-equiv-forwarding)))
You can also load just the definitions and bare-minimum theorems using
(include-book "std/basic/arith-equiv-defs" :dir :system)