Goldbach.ramare_saouter_odd_goldbach

@[blueprint  "ramare-saouter-odd-goldbach"  (title := "Ramaré and Saouter's verification of odd Goldbach")  (statement := /-- \cite[Corollary 1]{ramare-saouter}  The odd Goldbach conjecture is verified up to $1.13256 \times 10^{22}$. -/)  (proof := /-- Combine Proposition \ref{richstein-even-goldbach},  Proposition \ref{even-to-odd-goldbach-triv}, and Theorem \ref{thm:ramare-saouter2003}. -/)  (latexEnv := "proposition")  (discussion := 962)]theorem ramare_saouter_odd_goldbach : odd_conjecture 11325599999999886744004 := by  have h1 := even_to_odd_goldbach 10726905042 (4 * 10 ^ 14) 28314000    (fun x hx => RamareSaouter2003.has_prime_in_interval x (by norm_cast : (x : ℝ) > 10726905041))    richstein_goldbach  have h2 := odd_conjecture_mono (4 * 10 ^ 14 + 3) 10726905046    (even_to_odd_goldbach_triv _ richstein_goldbach)  norm_num at *  exact h1 h2