Error when using Exponents

Stream: new members

[Tyler Brown]

I'm referencing Calculational Proofs from Ch.4 Quantifiers and Equality of Theorem Proving in Lean 4 while trying to implement an example outside of the book which is Fermats Little Theorem. I found course materials online and I'm trying to extend their first hw assignment (cs.cmu.edu/~crary/317-f24/homeworks/hw1-handout.. You'll note that this course uses DCheck instead of Lean so I'm definitely not a student in the course looking for answers to their homework assignment. From the assignment:

Fermat’s Little Theorem states that if p is prime, then for any integer a, (a p − a) mod p = 0. Also note that (2422687 − 2) mod 422687 = 376010.

I am currently trying to implement a nonconstructive proof that the integer 422687 is composite.

example : ∃ a p : Int, (a ^ p - a) % p > 0 := sorry

Are you aware of more examples that use exponents in proofs without using tactics? In this particular example, is there a reason why I receive an error when trying to use the exponent $a^p$?

Thank you!

[Aaron Liu]

The reason you are having trouble with a ^ p is because a and p are integers, and an integer to an integer power is in general a rational number.