proposition: Lemma Rs_derivable : derivable Rs.
proof: Proof. unfold derivable in |- *; intro. case (total_order_T (cos (alphas x)) 0); intro. elim s; intro. cut (cos (alphas x) <> 0%R). intro; cut (exists eps : posreal, (forall h : R, (Rabs h < eps)%R -> cos (alphas (x + h)%R) <> 0%R)). set (xi_p := fun t : R => xi intr t). intro; cut (derivable_pt (fun t : R => ((xi_p t - xi_p 0) / cos (alphas t))%R) x). intro X; unfold derivable_pt in X; elim X; intros l H1. unfold derivable_pt in |- *; exists l. unfold derivable_pt_abs in H1; unfold derivable_pt_lim in H1; unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; intros. elim (H1 eps H2); intros del H3. elim H0; intros dom H4. cut (0 < Rmin del dom)%R. intro; exists (mkposreal (Rmin del dom) H5); intros. repeat rewrite Rs_x. unfold xi_p in H3; apply H3. assumption. apply Rlt_le_trans with (Rmin del dom); [ apply H7 | apply Rmin_l ]. apply H. apply H4; apply Rlt_le_trans with (Rmin del dom); [ apply H7 | apply Rmin_r ]. unfold Rmin in |- *; case (Rle_dec del dom); intro. apply (cond_pos del). apply (cond_pos dom). set (alphas_p := d2 alphas); reg. unfold alphas_p in |- *; apply (cond_D1 alphas). apply (xi_derivable intr x). set (alphas_p := d2 alphas); set (f := fun t : R => cos (alphas_p t)). cut (exists eps : posreal, (forall h : R, (Rabs h < eps)%R -> f (x + h)%R <> 0%R)). intro; elim H0; intros. exists x0; intros; unfold f in H1; apply H1; assumption. apply continuous_neq_0. unfold f in |- *; reg; apply derivable_continuous_pt; apply (cond_D1 alphas). apply H. red in |- *; intro; rewrite H in a; elim (Rlt_irrefl _ a). cut (sin (alphas x) <> 0%R). intro; cut (exists eps : posreal, (forall h : R, (Rabs h < eps)%R -> sin (alphas (x + h)%R) <> 0%R)). set (yi_p := fun t : R => yi intr t). intro; cut (derivable_pt (fun t : R => ((yi_p t - yi_p 0) / sin (alphas t))%R) x). intro X; unfold derivable_pt in X. elim X; intros l H1. unfold derivable_pt in |- *; exists l. unfold derivable_pt_abs in H1; unfold derivable_pt_lim in H1; unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; intros. elim (H1 eps H2); intros del H3. elim H0; intros dom H4. cut (0 < Rmin del dom)%R. intro; exists (mkposreal (Rmin del dom) H5); intros. repeat rewrite Rs_y. unfold yi_p in H3; apply H3. assumption. apply Rlt_le_trans with (Rmin del dom); [ apply H7 | apply Rmin_l ]. apply H. apply H4; apply Rlt_le_trans with (Rmin del dom); [ apply H7 | apply Rmin_r ]. unfold Rmin in |- *; case (Rle_dec del dom); intro. apply (cond_pos del). apply (cond_pos dom). set (alphas_p := d2 alphas); reg. unfold alphas_p in |- *; apply (cond_D1 alphas). apply (yi_derivable intr x). set (alphas_p := d2 alphas); set (f := fun t : R => sin (alphas_p t)). cut (exists eps : posreal, (forall h : R, (Rabs h < eps)%R -> f (x + h)%R <> 0%R)). intro; elim H0; intros. exists x0; intros; unfold f in H1; apply H1; assumption. apply continuous_neq_0. unfold f in |- *; reg; apply derivable_continuous_pt; apply (cond_D1 alphas). apply H. assert (H := cos_sin_0_var (alphas x)); elim H; intro. elim H0; assumption. exact H0. cut (cos (alphas x) <> 0%R). intro; cut (exists eps : posreal, (forall h : R, (Rabs h < eps)%R -> cos (alphas (x + h)%R) <> 0%R)). set (xi_p := fun t : R => xi intr t). intro; cut (derivable_pt (fun t : R => ((xi_p t - xi_p 0) / cos (alphas t))%R) x). intro X; unfold derivable_pt in X; elim X; intros l H1. unfold derivable_pt in |- *; exists l. unfold derivable_pt_abs in H1; unfold derivable_pt_lim in H1; unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; intros. elim (H1 eps H2); intros del H3. elim H0; intros dom H4. cut (0 < Rmin del dom)%R. intro; exists (mkposreal (Rmin del dom) H5); intros. repeat rewrite Rs_x. unfold xi_p in H3; apply H3. assumption. apply Rlt_le_trans with (Rmin del dom); [ apply H7 | apply Rmin_l ]. apply H. apply H4; apply Rlt_le_trans with (Rmin del dom); [ apply H7 | apply Rmin_r ]. unfold Rmin in |- *; case (Rle_dec del dom); intro. apply (cond_pos del). apply (cond_pos dom). set (alphas_p := d2 alphas); reg. unfold alphas_p in |- *; apply (cond_D1 alphas). apply (xi_derivable intr x). set (alphas_p := d2 alphas); set (f := fun t : R => cos (alphas_p t)). cut (exists eps : posreal, (forall h : R, (Rabs h < eps)%R -> f (x + h)%R <> 0%R)). intro; elim H0; intros. exists x0; intros; unfold f in H1; apply H1; assumption. apply continuous_neq_0. unfold f in |- *; reg; apply derivable_continuous_pt; apply (cond_D1 alphas). apply H. red in |- *; intro; rewrite H in r; elim (Rlt_irrefl _ r). Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho