no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x < π / 2
⊢ y ≤ π + π / 2
linarith [pi_pos]
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x < π / 2
⊢ -(π / 2) < x
linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x = π / 2
⊢ π / 2 < y
linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x = π / 2
⊢ y < π + π / 2
linarith [pi_pos]
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx✝ : x ≤ π / 2
hy : π / 2 ≤ y
hx : x = π / 2
⊢ 0 = cos x
rw [hx, cos_pi_div_two]
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : y ≤ π / 2
⊢ cos y < cos x
linarith
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ cos (π - x) < cos (π - y)
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ -cos x < -cos y
rw [← cos_pi_sub, ← cos_pi_sub]
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx : π / 2 ≤ x
hy : π / 2 ≤ y
⊢ cos (π - x) < cos (π - y)
apply cos_lt_cos_of_nonneg_of_le_pi_div_two <;>
linarith