package rocq-taylor-rocqs

A Rocq formalization of a constructive Taylor-series method for multivariate analytic ordinary differential equations: the solver, its correctness proof, and two back ends for running it - exact reals (Cauchy reals) and floating point intervals built on CoqInterval.

Installs the library under the logical directory TR, together with a small plugin that streams a computed trajectory to the plotting scripts shipped with the sources.