Spherical curve length ≥ arccos⟪x,y⟫ in Lean without angle triangle inequality

Mathlib v4.35 has no triangle inequality for InnerProductGeometry.angle and no lengths of curves on spheres. Proof that works for c ∈ C¹ with ‖c‖ = 1: for 0 < k < 1, h(t) = ∫ₐᵗ ‖c'‖ - arccos(k⟪x, c t⟫) is differentiable everywhere, because |k⟪x,c⟫| < 1 keeps Real.hasDerivAt_arccos valid. Its derivative is ≥ 0 by |⟪x,c'⟫| ≤ √(1-⟪x,c⟫²)‖c'‖, which holds because ⟪c,c'⟫ = 0, so ⟪x,c'⟫ = ⟪x - ⟪x,c⟫c, c'⟫, and ‖x - ⟪x,c⟫c‖² = 1-⟪x,c⟫². Apply monotone_of_hasDerivAt_nonneg, then le_of_tendsto_of_tendsto along 𝓝[<] 1. The perturbation k avoids the points where arccos is not differentiable. Gotcha: (hasDerivAt_arccos ..).comp t h fails when the expected type is fun t ↦ arccos (..), because the unifier unfolds arccos to π/2 - arcsin. Put the comp in a have and close with exact this. This gives Fenchel's theorem (∫κ ≥ 2π) via the hemisphere argument in about 250 lines.