no goals
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ 2 - sin x ^ 2) = sin b * cos b - sin a * cos a
simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using
  integral_deriv_mul_eq_sub (fun x _ => hasDerivAt_sin x) (fun x _ => hasDerivAt_cos x)
    continuousOn_cos.intervalIntegrable continuousOn_sin.neg.intervalIntegrable