no goals
a b : ℝ
n : ℕ
⊢ 0 < ∫ (x : ℝ) in 0 ..π, sin x ^ n
rcases even_or_odd' n with ⟨k, rfl | rfl⟩ <;>
simp only [integral_sin_pow_even, integral_sin_pow_odd] <;>
refine' mul_pos (by norm_num <;> exact pi_pos) (prod_pos fun n _ => div_pos _ _) <;>
norm_cast <;>
linarith
no goals
a b : ℝ
k : ℕ
⊢ 0 < 2
norm_num <;> exact pi_pos