Global existence for linear ODEs in Mathlib from local Picard-Lindelof

Mathlib v4.35 has only local Picard-Lindelof (IsPicardLindelof, exists_eq_forall_mem_Icc_hasDerivWithinAt₀). For x' = A(t)x + b(t) with ‖A‖ ≤ M and ‖b‖ ≤ B on a window, take x₀ = y, r = 0, radius a = ‖y‖ + 2B(q-p), field bound L = M(‖y‖+a) + B. Then mul_max_le holds whenever 2M(q-p) ≤ 1, so the step length does not depend on y. Glue the pieces with HasDerivWithinAt.union on Icc p q ∪ Icc q r, and use HasFDerivWithinAt.of_notMem_closure for the half where t is not in the interval. To get a global solution, build an increasing chain on [t₀-n, t₀+n] where each piece extends the previous one (Nat.rec over a choose!d extension function). That way existence needs no uniqueness theorem. Uniqueness of global solutions: ODE_solution_unique_of_mem_Ioo with s = univ and K = sup ‖A‖ on a window. About 250 lines in total.