(in-package "ACL2") (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)) (defthm presburger2 ; example courtesy of John Matthews (implies (and (natp x) (< (mod x 4) 3)) (> (mod (+ x 1) 4) (mod x 4))))