proposition: Lemma Dx0_PI : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI)%R -> (vi intr * cos (rho_vi * t) <= derive_pt xp t (xp_derivable t))%R.
proof: Proof. intros; rewrite Dxp; apply Rmult_le_compat_l; [ left; apply TypeSpeed_pos | generalize (theta_inv t H); intro; elim H1; intros; case (Rcase_abs (thetat intr t - thetat intr 0)); intro; [ cut (thetat intr 0 - thetat intr t <= rho_vi * t)%R; [ cut (- (rho_vi * t) <= thetat intr 0 - thetat intr t)%R; [ intros; rewrite <- (cos_neg (thetat intr t - thetat intr 0)); replace (- (thetat intr t - thetat intr 0))%R with (thetat intr 0 - thetat intr t)%R; [ apply cos_decr_1; [ left; generalize (Ropp_lt_gt_contravar (thetat intr t - thetat intr 0) 0 r); rewrite Ropp_0; replace (- (thetat intr t - thetat intr 0))%R with (thetat intr 0 - thetat intr t)%R; [ intro; assumption | ring ] | apply Rle_trans with (rho_vi * t)%R; assumption | apply (rho_t_pos t H) | assumption | assumption ] | ring ] | apply Rplus_le_reg_l with (thetat intr t + rho_vi * t)%R; repeat rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; replace (thetat intr t + (rho_vi * t + (thetat intr 0 - thetat intr t)))%R with (thetat intr 0 + rho_vi * t)%R; [ assumption | ring ] ] | apply Rplus_le_reg_l with (thetat intr t - rho_vi * t)%R; unfold Rminus in |- *; repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite Rplus_comm; repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite Rplus_comm; assumption ] | generalize (Rge_le (thetat intr t - thetat intr 0) 0 r); intro; cut (thetat intr t - thetat intr 0 <= rho_vi * t)%R; [ cut (- (rho_vi * t) <= thetat intr t - thetat intr 0)%R; [ intros; apply cos_decr_1; [ assumption | apply Rle_trans with (rho_vi * t)%R; assumption | apply (rho_t_pos t H) | assumption | assumption ] | apply Rplus_le_reg_l with (thetat intr 0); unfold Rminus in |- *; rewrite (Rplus_comm (thetat intr t)); repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l; assumption ] | apply Rplus_le_reg_l with (thetat intr 0); unfold Rminus in |- *; rewrite (Rplus_comm (thetat intr t)); repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l; assumption ] ] ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega