proposition: Lemma Dyi : forall t : R, derive_pt (yi intr) t (yi_derivable intr 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.
proof: Proof. intro. set (H := Rs_derivable t). cut (derivable_pt alphas_p t); [ intro X | apply (cond_D1 alphas) ]. cut (derivable_pt ((Rs * comp sin alphas_p)%F + fct_cte (yi intr 0)) t); [ intro X0 | reg ]. replace (derive_pt (yi intr) t (yi_derivable intr t)) with (derive_pt ((Rs * comp sin alphas_p)%F + fct_cte (yi intr 0)) t X0). replace (derive_pt alphas t (cond_D1 alphas t)) with (derive_pt alphas_p t X); [ idtac | apply pr_nu ]. unfold plus_fct, mult_fct, comp, fct_cte in |- *. reg. unfold comp, alphas_p in |- *; ring. unfold derive_pt in |- *. case X0. case (yi_derivable intr 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 H0); intros. exists x1; intros. unfold plus_fct, mult_fct, comp, fct_cte in |- *. assert (H4 := H1 _ H2 H3). replace ((Rs (t + h) * sin (alphas_p (t + h)) + yi intr 0 - (Rs t * sin (alphas_p t) + yi intr 0)) / h - x)%R with ((yi intr (t + h) - yi intr t) / h - x)%R. apply H4. rewrite (Rsy t). rewrite (Rsy (t + h)). replace (yi intr 0 + Rs (t + h) * sin (alphas (t + h)) - (yi intr 0 + Rs t * sin (alphas t)))%R with (Rs (t + h) * sin (alphas_p (t + h)) + yi intr 0 - (Rs t * sin (alphas_p t) + yi intr 0))%R. reflexivity. unfold alphas_p in |- *; ring. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho