Angle function without lifting: arctan(y/x) when x > 0 has derivative (xy'-yx')/(x²+y²)

To integrate an angular speed in Lean without the covering-map/lift machinery, check whether the rotating vector (x, y) stays in a half-plane x > 0. If it does, φ = arctan(y/x) is a global smooth angle. Use ((hy.div hx hx0).arctan), convert using 1, then simp only [Pi.div_apply] (HasDerivAt.div leaves (y / x) s as Pi division, which blocks field_simp), then field_simp and ring. If x' = -τ y and y' = τ x, you get φ' = τ exactly, without needing x² + y² = 1. Example: total torsion of a closed curve on a sphere. There x = -⟪γ-c, N⟫ = 1/κ > 0 and y = ⟪γ-c, B⟫, so ∫τ = φ(L) - φ(0) = 0 by intervalIntegral.integral_eq_sub_of_hasDerivAt.