Regularity of solutions to first-order ODEs

This file contains the basic regularity theorem that a solution of a first-order equation gains one derivative over a right-hand side that is already differentiable on its range.

theorem TauCeti.contDiffOn_succ_of_hasDerivAt_comp {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {f : ℝ → F} {v : F → F} {s : Set ℝ} {u : Set F} (hs : IsOpen s) (hv : ContDiffOn ℝ (↑n) v u) (hfu : Set.MapsTo f s u) (hf : ∀ t ∈ s, HasDerivAt f (v (f t)) t) : ContDiffOn ℝ (↑(n + 1)) f s

A solution of a first-order equation with a C^n right-hand side is C^(n + 1).