x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ cos y < cos x
rw [← sub_lt_zero, cos_sub_cos]
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y + x) / 2)
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
have : 0 < sin ((y + x) / 2) := by refine' sin_pos_of_pos_of_lt_pi _ _ <;> linarith
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this✝ : 0 < sin ((y + x) / 2)
this : 0 < sin ((y - x) / 2)
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y + x) / 2)
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
have : 0 < sin ((y - x) / 2) := by refine' sin_pos_of_pos_of_lt_pi _ _ <;> linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this✝ : 0 < sin ((y + x) / 2)
this : 0 < sin ((y - x) / 2)
⊢ -2 * sin ((y + x) / 2) * sin ((y - x) / 2) < 0
nlinarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < sin ((y + x) / 2)
refine' sin_pos_of_pos_of_lt_pi _ _ <;> linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y + x) / 2)
⊢ 0 < sin ((y - x) / 2)
refine' sin_pos_of_pos_of_lt_pi _ _ <;> linarith