theorem Goldbach.IsGoldbachPair.symm {n p q : ℕ} (h : IsGoldbachPair n p q) : IsGoldbachPair n q p

theorem Goldbach.HasGoldbachDecomposition.four_le {n : ℕ} (h : HasGoldbachDecomposition n) : 4 ≤ n

theorem Goldbach.hasGoldbachDecomposition_double_of_prime {p : ℕ} (hp : Nat.Prime p) : HasGoldbachDecomposition (p + p)

theorem Goldbach.hasGoldbachDecomposition_four : HasGoldbachDecomposition 4

theorem Goldbach.hasGoldbachDecomposition_six : HasGoldbachDecomposition 6

theorem Goldbach.hasGoldbachDecomposition_eight : HasGoldbachDecomposition 8

theorem Goldbach.hasGoldbachDecomposition_ten : HasGoldbachDecomposition 10

theorem Goldbach.hasGoldbachDecomposition_twelve : HasGoldbachDecomposition 12

theorem Goldbach.hasGoldbachDecomposition_fourteen : HasGoldbachDecomposition 14

theorem Goldbach.hasGoldbachDecomposition_sixteen : HasGoldbachDecomposition 16

theorem Goldbach.hasGoldbachDecomposition_eighteen : HasGoldbachDecomposition 18

theorem Goldbach.hasGoldbachDecomposition_twenty : HasGoldbachDecomposition 20