proposition: Lemma Dyp : forall t : R, derive_pt yp t (yp_derivable t) = (v (vi intr) * sin (thetat intr t - thetat intr 0))%R.
proof: Proof. intro; unfold yp 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 xi_p t H) with (derive_pt (x intr) t (cond_diff (x intr) t)); [ idtac | apply pr_nu ]. replace (derive_pt yi_p t H0) with (derive_pt (y intr) t (cond_diff (y intr) t)); [ idtac | apply pr_nu ]. rewrite H2; rewrite H3. rewrite sin_minus. unfold fct_cte, vi, thetat_p, thetat in |- *. ring. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega