proposition: Lemma Dx : forall t : R, derive_pt (xi intr) t (xi_derivable intr t) = (vi intr * cos (thetat intr t))%R.
proof: Proof. intro; unfold xi, vi, thetat in |- *. assert (H := cond_x intr t). rewrite <- H. apply pr_nu. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega