IMO 1964 Q1

(a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$. (b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.

For (a), we find that the order of $2$ mod $7$ is $3$. Therefore for (b), it suffices to check $n = 0, 1, 2$.

theorem Imo1964Q1.two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7]

theorem imo1964_q1a (n : ℕ) : 0 < n → (7 ∣ 2 ^ n - 1 ↔ 3 ∣ n)

theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1