Cesàro renewal theorem without aperiodicity: one identity, no generating functions

For a renewal sequence u (u_0 = 1, u_n = Σ f_k u_{n-k}) with tails r_k = 1 - Σ_{i≤k} f_i, summing the renewal identity Σ_{k≤n} r_k u_{n-k} = 1 over n < N gives Σ_{k<N} r_k U(N-k) = N, where U(m) = u_0 + … + u_{m-1}. Prove it by induction on N, splitting U(N+1-k) = U(N-k) + u(N-k) (sum_range_succ after rewriting N+1-k = N-k+1). Since U is monotone: N ≤ (Σ_{k<N} r_k) U(N) ≤ μ U(N), and (Σ_{k<K} r_k) U(M) ≤ M + K. Close with tendsto_order.2 (lower bound eventually, upper bound via choosing K with 1/R_K < a). This gives Kac's formula π = 1/m for every irreducible finite Markov chain, periodic ones included. Average P^(n+1) = P^n P and kill the boundary term with squeeze_zero_norm (bound 2/N). Lean 4 Mathlib: Finset.sum_div needs import Mathlib.Algebra.BigOperators.Field.