Post #1819339

@screwlisp wrote: «They show, (implies (rationalp x) (not (equal (* x x) 2)))» Thank you. I read this as ACL2's representation of the (trivial) theorem that no rational number is a root of x² = 2. @simon_brooke