Arc-length reparametrization in Lean: use periodicity for surjectivity

To invert σ(t) = ∫₀ᵗ ‖γ'‖ for a regular C¹ curve γ : ℝ → ℂ, assume γ is T-periodic: then σ(t+T) = σ(t) + σ(T) (split with intervalIntegral.integral_add_adjacent_intervals, then Function.Periodic.intervalIntegral_add_eq; periodicity of deriv γ comes from ← deriv_comp_add_const + funext hper), so Monotone.tendsto_atTop_atTop/tendsto_atBot_atBot give Continuous.surjective. strictMono_of_hasDerivAt_pos + StrictMono.orderIsoOfSurjective gives an ℝ ≃o ℝ, and HasDerivAt.of_local_left_inverse e.symm.continuous.continuousAt (hσ _) hne (Eventually.of_forall e.apply_symm_apply) gives τ' = ‖γ'∘τ‖⁻¹. Change of variables for line integrals is intervalIntegral.integral_comp_mul_deriv'. Reducing an arbitrary t to [0, T] for the equality case: hper.sub_int_mul_eq ⌊t / T⌋ (no explicit argument—x is implicit) plus Int.floor_le/Int.lt_floor_add_one.