γ₃_increasing

lemma γ₃_increasing (n : ℕ) (hn : 1 ≤ n) :    γ₃ n < γ₃ (n + 1) := by  unfold γ₃  suffices h : 0 < (2 * ↑n + 1) / (2 * ↑n * (↑n + 1))      - Real.log ((↑n + 1 : ℝ) / ↑n)      - (2 * ↑n + 1) / (12 * ↑n ^ 2 * (↑n + 1) ^ 2)      + (4 * ↑n ^ 3 + 6 * ↑n ^ 2 + 4 * ↑n + 1) /        (120 * ↑n ^ 4 * (↑n + 1) ^ 4) by    rw [Real.log_div] at h <;> norm_num at * <;> try positivity    field_simp at *; grind  have hn_pos : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega)  have h_log_ineq := log_ineq_9 (1 / (n : ℝ)) (by positivity)  rw [show (1 : ℝ) + 1 / (↑n : ℝ) = (↑n + 1) / ↑n by field_simp] at h_log_ineq  rw [Real.log_div (by positivity) (ne_of_gt hn_pos)] at h_log_ineq  rw [Real.log_div (by positivity) (ne_of_gt hn_pos)]  field_simp at *  nlinarith [sq_nonneg ((n : ℝ)), sq_nonneg ((n : ℝ) - 1),    pow_pos hn_pos 2, pow_pos hn_pos 3, pow_pos hn_pos 4,    pow_pos hn_pos 5, pow_pos hn_pos 6, pow_pos hn_pos 7, pow_pos hn_pos 8,    pow_pos (show (0 : ℝ) < n + 1 by linarith) 2,    pow_pos (show (0 : ℝ) < n + 1 by linarith) 3,    pow_pos (show (0 : ℝ) < n + 1 by linarith) 4]