proposition: Lemma Dyp0_PI2 : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI / 2)%R -> (- (vi intr * sin (rho_vi * t)) <= derive_pt yp t (yp_derivable t) <= vi intr * sin (rho_vi * t))%R.
proof: Proof. Proof with trivial. intros... rewrite Dyp... generalize (theta_inv t H); intro; elim H1; intros... cut (thetat intr t - thetat intr 0 <= rho_vi * t)%R... cut (- (rho_vi * t) <= thetat intr t - thetat intr 0)%R... intros... split... replace (- (vi intr * sin (rho_vi * t)))%R with (vi intr * - sin (rho_vi * t))%R... apply Rmult_le_compat_l... left; apply TypeSpeed_pos... rewrite <- (sin_neg (rho_vi * t))... apply sin_incr_1... apply Ropp_ge_le_contravar; apply Rle_ge... apply Rle_trans with 0%R... rewrite <- Ropp_0... apply Ropp_ge_le_contravar; apply Rle_ge; apply (rho_t_pos t H)... left; apply PI2_RGT_0... apply Rle_trans with (- (rho_vi * t))%R... apply Ropp_ge_le_contravar... apply Rle_ge... apply Rle_trans with (rho_vi * t)%R... ring... apply Rmult_le_compat_l... left; apply TypeSpeed_pos... apply sin_incr_1... apply Rle_trans with (- (rho_vi * t))%R... apply Ropp_ge_le_contravar; apply Rle_ge... apply Rle_trans with (rho_vi * t)%R... apply Rle_trans with 0%R... rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; left; apply PI2_RGT_0... apply (rho_t_pos t H)... 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... 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... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega