IMO 2016 N4

Consider some $k, ℓ, m, n ∈ ℕ^+$ with $n > 1$ such that $$ n^k + mn^ℓ + 1 ∣ n^{k + ℓ} - 1. $$ Prove that one of the following holds:

• $m = 1$ and $ℓ = 2k$; or
• $k = (t + 1)ℓ$ and $m(n^ℓ - 1) = n^{t ℓ} - 1$ for some $t > 0$.

theorem IMOSL.IMO2016N4.dvd_of_pow_sub_one_dvd {n k l : ℕ} (hn : 1 < n) (h : n ^ k - 1 ∣ n ^ l - 1) : k ∣ l

theorem IMOSL.IMO2016N4.final_solution {k l m n : ℕ} (hk : 0 < k) (hl : 0 < l) (hm : 0 < m) (hn : 1 < n) (h : n ^ k + m * n ^ l + 1 ∣ n ^ (k + l) - 1) : m = 1 ∧ l = 2 * k ∨ ∃ (t : ℕ), t > 0 ∧ k = (t + 1) * l ∧ m * (n ^ l - 1) = n ^ (l * t) - 1

Final solution