case h.h.ha

⊢ 0 ≤ cos 1

case h.h.hab

⊢ cos 1 ≤ 2 / 3
⊢ 2 * cos 1 ^ 2 - 1 ≤ 2 * (2 / 3) ^ 2 - 1
gcongr
no goals
case h.h.ha

⊢ 0 ≤ cos 1
exact cos_one_pos.le
no goals
case h.h.hab

⊢ cos 1 ≤ 2 / 3
apply cos_one_le
no goals
⊢ 2 * (2 / 3) ^ 2 - 1 < 0
norm_num