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