Lcm.Criterion.prod_p_le_prod_q

@[blueprint  "lem:4p3q3"  (statement := /-- We have $4 p_1 p_2 p_3 < q_1 q_2 q_3$. -/)  (proof := /-- Obvious from the non-negativity of the left-hand side of \eqref{eq:main-ineq}. -/)  (latexEnv := "lemma")]theorem Criterion.prod_p_le_prod_q (c : Criterion) : 4 * ∏ i, c.p i < ∏ i, c.q i := by  have hBC_pos : 0 < (∏ i, (1 + (1 : ℝ) / (c.p i * (c.p i + 1)))) * (1 + 3 / (8 * c.n)) := by    positivity  have hR_pos : 0 < 1 - 4 * (∏ i, (c.p i : ℝ)) / ∏ i, (c.q i : ℝ) := by    by_contra h    exact absurd (c.h_crit.trans (mul_nonpos_of_nonneg_of_nonpos hBC_pos.le (not_lt.mp h)))      (not_le.mpr <| prod_pos fun i _ ↦ by positivity)  rw [sub_pos, div_lt_one <| prod_pos fun i _ ↦ cast_pos.mpr (c.hq i).pos] at hR_pos  exact_mod_cast hR_pos