x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ cos (-(x - π / 2)) < cos (-(y - π / 2))
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ sin x < sin y
rw [← cos_sub_pi_div_two, ← cos_sub_pi_div_two, ← cos_neg (x - _), ← cos_neg (y - _)]
no goals
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ cos (-(x - π / 2)) < cos (-(y - π / 2))
apply cos_lt_cos_of_nonneg_of_le_pi <;> linarith