proposition: Lemma DRs : forall t : R, derive_pt Rs t (Rs_derivable t) = (vi intr * cos (thetat t - alphas t))%R.
proof: Proof. intro. assert (H := DRs_cos t). assert (H0 := DRs_sin t). assert (H1 := Rmult_eq_compat_l (cos (alphas t)) _ _ H). assert (H2 := Rmult_eq_compat_l (sin (alphas t)) _ _ H0). replace (derive_pt Rs t (Rs_derivable t)) with (cos (alphas t) * (derive_pt Rs t (Rs_derivable t) * cos (alphas t) - Rs t * sin (alphas t) * derive_pt alphas t (cond_D1 alphas t)) + sin (alphas t) * (derive_pt Rs t (Rs_derivable t) * sin (alphas t) + Rs t * cos (alphas t) * derive_pt alphas t (cond_D1 alphas t)))%R. replace (vi intr * cos (thetat t - alphas t))%R with (cos (alphas t) * (vi intr * cos (thetat t)) + sin (alphas t) * (vi intr * sin (thetat t)))%R. apply eq_plus_eq_is_eq; assumption. rewrite cos_minus; ring. unfold Rminus in |- *. repeat rewrite Rmult_plus_distr_l. replace (cos (alphas t) * (derive_pt Rs t (Rs_derivable t) * cos (alphas t)) + cos (alphas t) * - (Rs t * sin (alphas t) * derive_pt alphas t (cond_D1 alphas t)) + (sin (alphas t) * (derive_pt Rs t (Rs_derivable t) * sin (alphas t)) + sin (alphas t) * (Rs t * cos (alphas t) * derive_pt alphas t (cond_D1 alphas t))))%R with (derive_pt Rs t (Rs_derivable t) * (Rsqr (sin (alphas t)) + Rsqr (cos (alphas t))) + cos (alphas t) * - (Rs t * sin (alphas t) * derive_pt alphas t (cond_D1 alphas t)) + sin (alphas t) * (Rs t * cos (alphas t) * derive_pt alphas t (cond_D1 alphas t)))%R; [ idtac | unfold Rsqr in |- *; ring ]. rewrite sin2_cos2; ring. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho