Feit-Thompson conjecture on primes

Reference: Wikipedia

theorem feit_thompson_primes (p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (h : p < q) : ¬(q ^ p - 1) / (q - 1) ∣ (p ^ q - 1) / (p - 1)

There are no distinct primes $p$ and $q$ such that $\frac{q^p - 1}{q - 1}$ divides $\frac{p^q - 1}{p - 1}$