fact: Axiom D_abs_alpha : forall t : R, (0 <= t)%R -> (t < 2 / rho (vi intr))%R -> (- rho (vi intr) / 2 <= derive_pt alphas t (cond_D1 alphas t))%R /\ (derive_pt alphas t (cond_D1 alphas t) <= rho (vi intr) / 2)%R.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho