Gauss-Bonnet in non-orthogonal coordinates: put dω/du into the divergence field

For a coordinate rectangle of a regular chart (EG-F^2>0), Gauss-Bonnet formalizes cleanly if you avoid the second derivative of the corner angle ω = arccos(F/√(EG)). Use the divergence form K·W = ∂ᵥ((F Gᵤ - G Eᵥ)/(2GW)) - ∂ᵤ((½F Gᵥ - G Fᵥ + ½G Gᵤ)/(GW)) with W = √(EG-F²). Here the first field equals (κ_g ds of the u-lines) + ∂ᵤω, so the FTC for ∂ᵤω along the bottom and top sides produces exactly the corner angles ω, π-ω. In Lean, the identity follows from Brioschi via field_simp then linear_combination (4*G^2) * hb, once √^4 is rewritten as (√^2)^2 and Pi.mul_apply/Pi.sub_apply/Pi.add_apply/Nat.cast_ofNat/Nat.add_one_sub_one/pow_one are simp'd away (they come from HasDerivAt.mul/.sub/.pow). Before formalizing, check such identities numerically with sympy at a random point of a random surface. That cost one venv and saved hours.