Real.Stirling.half_shift_log_constant_pos

lemma half_shift_log_constant_pos : 0 < half_shift_log_constant := by  have hthree : 0 < (3 / 2 : ℝ) := by norm_num  have hcoef : 0 < Real.log 3 / Real.log 2 + 1 := by    have hlog2_pos : 0 < Real.log 2 := Real.log_pos (by norm_num : (1 : ℝ) < 2)    have hlog3_pos : 0 < Real.log 3 := Real.log_pos (by norm_num : (1 : ℝ) < 3)    have hcoef_nonneg : 0 ≤ Real.log 3 / Real.log 2 :=      div_nonneg hlog3_pos.le hlog2_pos.le    linarith  simpa [half_shift_log_constant] using mul_pos hthree hcoef