no goals
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ x < sin (π / 2 * x)
simpa [mul_comm x] using
  strictConcaveOn_sin_Icc.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩
    pi_div_two_pos.ne (sub_pos.2 hx') hx