theorem Goldbach.strong_goldbach_conjecture (n : ℕ) : 4 ≤ n → Even n → HasGoldbachDecomposition n

Strong Goldbach conjecture: every even natural number n >= 4 is a sum of two prime numbers.

theorem Goldbach.strong_goldbach_conjecture_double (k : ℕ) : 2 ≤ k → HasGoldbachDecomposition (k + k)

Equivalent doubled-index form of Strong Goldbach.