proposition: Lemma D_Rs_alphas2 : forall t : R, derive_pt (fun y : R => (Rs y * derive_pt alphas y (cond_D1 alphas y))%R) t (fct_der5 t) = (vi intr * cos (thetat t - alphas t) * (derive_pt thetat t (thetat_derivable t) - derive_pt alphas t (cond_D1 alphas t)))%R.
proof: Proof. intro. cut (derivable_pt (fun x : R => (vi intr * sin (thetat x - alphas x))%R) t). intro X. replace (derive_pt (fun y : R => (Rs y * derive_pt alphas y (cond_D1 alphas y))%R) t (fct_der5 t)) with (derive_pt (fun x : R => (vi intr * sin (thetat x - alphas x))%R) t X). set (f := d2 alphas). cut (derivable_pt f t); [ intro X0 | apply (cond_D1 alphas) ]. cut (derivable_pt thetat t); [ intro X1 | apply thetat_derivable ]. reg. unfold fct_cte, minus_fct in |- *. replace (derive_pt f t (cond_D1 alphas t)) with (derive_pt f t X0); [ idtac | apply pr_nu ]. replace (derive_pt thetat t (thetat_derivable t)) with (derive_pt thetat t X1); [ idtac | apply pr_nu ]. ring. unfold derive_pt in |- *. case X; case (fct_der5 t); simpl; intros. eapply uniqueness_limite. unfold derivable_pt_abs in d0; apply d0. unfold derivable_pt_lim in |- *; intros. unfold derivable_pt_abs in d; unfold derivable_pt_lim in d; elim (d eps H); intros. exists x1; intros. do 2 rewrite <- Rs_alphas. apply H0; assumption. fold alphas_p in |- *; reg. apply (cond_D1 alphas). apply thetat_derivable. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho