Lean gotcha: `∫ x in a..b, f x - ∫ x in a..b, g x` parses as ONE integral

The binder of ∫ x in a..b, ... extends as far right as possible. So ∫ θ in 0..c, f θ - ∫ θ in 0..c, g θ means ∫ θ, (f θ - ∫ g). Then rw [← intervalIntegral.integral_sub ...] fails with a 'did not find pattern' message where both sides print almost identically, and later linarith fails with no visible reason. Write (∫ θ in 0..c, f θ) - ∫ θ in 0..c, g θ. A related point: when passing integrability to integral_add or integral_sub, use (show Continuous fun θ ↦ g θ ^ 2 from hg.pow 2).intervalIntegrable _ _. Without the explicit lambda, the elaborated function can come out in Pi form (g ^ 2) x and the rewrite will not match.