theorem ErdosStraus.erdos_straus_conjecture (n : ℕ) : 2 ≤ n → HasDecomposition n

The Erdős-Straus conjecture: every n >= 2 has a decomposition.

theorem ErdosStraus.erdos_straus_prime_case (p : ℕ) : Nat.Prime p → HasDecomposition p

Open prime case: every prime has a decomposition.