Integral of sine

Statement

For all real numbers $a$ and $b$, $$\int_a^b \sin x \, dx = \cos a - \cos b.$$

Remarks

The derivative of cosine is $-\sin$, so $-\cos$ is an antiderivative of $\sin$. For example, $\int_0^\pi \sin x \, dx = 2$. Mathlib states it as integral_sin.

Explanations

L1 human

The area under one arch of the sine curve is exactly $2$. This follows from the antiderivative $-\cos x$.