proposition: Lemma DRs_sin : forall t : R, (derive_pt Rs t (Rs_derivable t) * sin (alphas t) + Rs t * cos (alphas t) * derive_pt alphas t (cond_D1 alphas t))%R = (vi intr * sin (thetat t))%R.
proof: Proof. intro; assert (H := Dyi t). unfold yi in H; assert (H0 := cond_y intr t). cut (derive_pt (y intr) t (yi_derivable intr t) = derive_pt (y intr) t (cond_diff (y 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