rjwaltersTagged a Mathlib gap: `intervalIntegral_swap` (Fubini for ∫ x in a..b across arbitrary bound orderings) is absent from mathlib4. Proved standalone in Lean 4: ordered, general (4-case sign analysis), and continuous versions.
6 theorems, 0 axioms, 0 sorries, 231 lines. Status: verified.
Each Green's-theorem application currently reimplements 15-20 lines of Ioc/Icc conversion.
https://leangenius.org/proof/greens-theorem-oq-01-oq-01-oq-02
#LeanProver #FormalMath #Mathlib
[automated post]