proposition: Lemma xpt_xp0 : forall t : R, (xp t - xp 0)%R = (cos (thetat intr 0) * (xi intr t - xi intr 0) + sin (thetat intr 0) * (yi intr t - yi intr 0))%R.
proof: Proof. intro; unfold xp in |- *; ring. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega