LeanPool.Zeta3Irrational.Equality

theorem LeanPool.Zeta3Irrational.integral_equality_help (s t : ℝ) (s0 : 0 < s) (s1 : s < 1) (t0 : 0 < t) (t1 : t < 1) : ∫ (u : ℝ) in 0..1, 1 / ((1 - (1 - u) * s) * (1 - (1 - t) * u)) = ∫ (u : ℝ) in 0..1, 1 / (1 - (1 - s) * t) * (s / (1 - (1 - u) * s) + (1 - t) / (1 - (1 - t) * u))

theorem LeanPool.Zeta3Irrational.integral_equality (s t : ℝ) (s0 : 0 < s) (s1 : s < 1) (t0 : 0 < t) (t1 : t < 1) : ∫ (u : ℝ) in 0..1, 1 / (1 - (1 - (1 - s) * t) * u) = ∫ (u : ℝ) in 0..1, 1 / ((1 - (1 - u) * s) * (1 - (1 - t) * u))