proposition: Lemma DRs_cos : forall t : R, (derive_pt Rs t (Rs_derivable t) * cos (alphas t) - Rs t * sin (alphas t) * derive_pt alphas t (cond_D1 alphas t))%R = (vi intr * cos (thetat t))%R.
proof: Proof. intro. assert (H := Dxi t). unfold xi in H. assert (H0 := cond_x intr t). cut (derive_pt (x intr) t (xi_derivable intr t) = derive_pt (x intr) t (cond_diff (x intr) t)); [ intro | apply pr_nu ]. rewrite H1 in H. rewrite H0 in H. unfold vi, thetat in |- *; symmetry in |- *; assumption. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho