proposition: Lemma ypt_PI2 : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI / 2)%R -> (l * sin (beta + thetat intr 0) + r_vi * (cos (rho_vi * t) - 1) <= yp t)%R /\ (yp t <= l * sin (beta + thetat intr 0) - r_vi * (cos (rho_vi * t) - 1))%R.
proof: Proof. intros; generalize (ypt t H H0); intro; elim H1; intros; split; [ unfold hy in H2; unfold Rminus in H2; rewrite yp0 in H2; rewrite Rmult_0_r in H2; rewrite cos_0 in H2; rewrite Rmult_1_r in H2; generalize (Rplus_le_compat_r (l * sin (thetat intr 0 + beta)) (r_vi * cos (rho_vi * t) + - r_vi) (yp t + - (l * sin (thetat intr 0 + beta))) H2); replace (r_vi * cos (rho_vi * t) + - r_vi)%R with (r_vi * (cos (rho_vi * t) - 1))%R; [ repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro; rewrite <- (Rplus_comm (r_vi * (cos (rho_vi * t) - 1))); rewrite (Rplus_comm beta); assumption | ring ] | unfold hy in H3; unfold Rminus in H3; rewrite yp0 in H3; rewrite Rmult_0_r in H3; rewrite cos_0 in H3; rewrite Rmult_1_r in H3; generalize (Rplus_le_compat_r (l * sin (thetat intr 0 + beta)) (yp t + - (l * sin (thetat intr 0 + beta))) (r_vi + - (r_vi * cos (rho_vi * t))) H3); replace (r_vi + - (r_vi * cos (rho_vi * t)))%R with (- (r_vi * (cos (rho_vi * t) - 1)))%R; [ repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro; unfold Rminus in |- *; rewrite (Rplus_comm beta); rewrite <- (Rplus_comm (- (r_vi * (cos (rho_vi * t) + -1)))); assumption | unfold Rminus in |- *; rewrite Rmult_plus_distr_l; ring ] ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega