fact: Axiom alphas_exists : { f : Differential_D2 | forall t : R, xi intr t = (Rs t * cos (f t) + xi intr 0)%R /\ yi intr t = (Rs t * sin (f t) + yi intr 0)%R }.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho