proposition: Lemma Dxp : forall t : R, derive_pt xp t (xp_derivable t) = (vi intr * cos (thetat intr t - thetat intr 0))%R.
proof: Proof. intro; unfold xp in |- *. assert (H := xi_derivable intr t). assert (H0 := yi_derivable intr t). assert (H1 := thetat_derivable t). set (xi_p := xi intr) in H |- *. set (yi_p := yi intr) in H0 |- *. set (thetat_p := thetat intr) in H1 |- *. reg. assert (H2 := cond_x intr t). assert (H3 := cond_y intr t). replace (derive_pt yi_p t H0) with (derive_pt (y intr) t (cond_diff (y intr) t)); [ idtac | apply pr_nu ]. replace (derive_pt xi_p t H) with (derive_pt (x intr) t (cond_diff (x intr) t)); [ idtac | apply pr_nu ]. unfold vi in |- *. rewrite H2; rewrite H3; rewrite cos_minus; unfold thetat_p, thetat; ring. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega