proposition: Lemma xpt_PI : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI)%R -> (r_vi * sin (rho_vi * t) - l * cos (beta + thetat intr 0) <= xp t)%R.
proof: Proof. intros; generalize (xpt t H H0); intro; unfold Rminus, hx in H1; rewrite xp0 in H1; generalize (Rplus_le_compat_l (- l * cos (thetat intr 0 + beta)) (r_vi * sin (rho_vi * t)) (xp t + - (- l * cos (thetat intr 0 + beta))) H1); rewrite <- (Rplus_comm (r_vi * sin (rho_vi * t))); rewrite (Rplus_comm (- l * cos (thetat intr 0 + beta))); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite (Rplus_comm beta); unfold Rminus in |- *; intro; replace (- (l * cos (thetat intr 0 + beta)))%R with (- l * cos (thetat intr 0 + beta))%R; [ assumption | ring ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega