A difference of powers divisible by seventeen

The nice way (I used) to extract it is by FLT mod 17. $3^{16}\equiv 2^{16}\equiv 1 \pmod{17}$ by Fermat's Little Theorem. So $17|(3^{16}-2^{16})$

Source: InternLM Lean-Workbook, record lean_workbook_24006 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.