theorem Goldbach.hasGoldbachDecomposition_double_two_to_ten {k : ℕ} (hk2 : 2 ≤ k) (hk10 : k ≤ 10) : HasGoldbachDecomposition (k + k)

theorem Goldbach.hasGoldbachDecomposition_even_four_to_twenty {n : ℕ} (hn4 : 4 ≤ n) (hn20 : n ≤ 20) (hEven : Even n) : HasGoldbachDecomposition n