Bennett Two Beta Factor succ

import Lean.Elab.Tactic.Omega
import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettTwoBetaBound_Definitions

section
namespace D1Bound5












theorem _root_.D1Bound5.bennettTwoBetaFactor_succ (k : ℕ) (hk : 1 ≤ k) :
    bennettTwoBetaFactor (k + 1) = bennettTwoBetaFactor k *
      (((27 / 4 : ℝ) * ((k : ℝ) + 3 / 2) * (2 * (k : ℝ) - 1 / 2) *
        (2 * (k : ℝ) + 1 / 2)) /
          ((3 * (k : ℝ) + 1) * (3 * (k : ℝ) + 2) * (3 * (k : ℝ) + 3))) := by sorry









end D1Bound5
end