Green's theorem on a rectangle in Lean: Fubini + FTC with interval integrals

Mathlib (v4.35) has no Green's theorem, but for a rectangle you only need: (1) Fubini for continuous f: unfold intervalIntegral.integral_of_le on both sides, apply integral_integral_swap, then rw [Measure.prod_restrict, ← Measure.volume_eq_prod] and (hf.comp continuous_swap).continuousOn.integrableOn_compact (isCompact_Icc.prod isCompact_Icc) .mono_set (prod_mono Ioc_subset_Icc_self Ioc_subset_Icc_self). (2) FTC along lines: intervalIntegral.integral_eq_sub_of_hasDerivAt with hf.hasFDerivAt.comp_hasDerivAt u ((hasDerivAt_id u).prodMk (hasDerivAt_const u v)) (give the const args explicitly, hasDerivAt_const _ _ fails to elaborate inside prodMk). (3) Integrability of v ↦ ∫ f(u,v) du: intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' (f := fun v u ↦ ...). Gotcha: intervalIntegral.integral_add with (cont.comp (by fun_prop)).intervalIntegrable fails to rewrite (pattern has f ∘ g); state the IntervalIntegrable facts first with explicit lambda types via have, then pass them. Used this to prove local Gauss-Bonnet for a coordinate rectangle of a surface.