proposition: Lemma Math_prop_approx_y_a_PI2 : forall (a l1 l2 : R) (T : TimeT), (0 <= a)%R -> (a <= PI / 2)%R -> (0 <= l1)%R -> (l1 <= l2)%R -> (l1 * sin_lb a + r_ub V * (cos_lb (rho_ub V * MaxT) - 1) <= l2 * sin a + r_V * (cos (rho_V * T) - 1))%R.
proof: Proof. intros; apply Rplus_le_compat. apply Rle_trans with (l1 * sin a)%R. apply Rmult_le_compat_l. assumption. generalize (SIN a H (Rlt_le a PI (Rle_lt_trans a (PI / 2) PI H0 PI2_Rlt_PI))); intro; elim H3; intros; assumption. apply Rmult_le_compat_r. apply (sin_ge_0 a H (Rlt_le a PI (Rle_lt_trans a (PI / 2) PI H0 PI2_Rlt_PI))). assumption. rewrite <- (Ropp_involutive (r_ub V * (cos_lb (rho_ub V * MaxT) - 1))); rewrite <- (Ropp_involutive (r_V * (cos (rho_V * T) - 1))); apply Ropp_ge_le_contravar; apply Rle_ge; replace (- (r_V * (cos (rho_V * T) - 1)))%R with (r_V * (1 - cos (rho_V * T)))%R. replace (- (r_ub V * (cos_lb (rho_ub V * MaxT) - 1)))%R with (r_ub V * (1 - cos_lb (rho_ub V * MaxT)))%R. apply Rmult_le_compat. left; apply r_V_is_pos. apply Rplus_le_reg_l with (cos (rho_V * T)); rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *; repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; generalize (COS_bound (rho_V * T)); intro; elim H3; intros; assumption. unfold r_V in |- *; left; apply r_ub_0. apply Rplus_le_reg_l with (Ropp 1); unfold Rminus in |- *; repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l; repeat rewrite Rplus_0_l; apply Ropp_ge_le_contravar; apply Rle_ge; apply Rle_trans with (cos (rho_ub V * MaxT)). cut (- PI / 2 <= rho_ub V * MaxT <= PI / 2)%R. intro; elim H3; intros; generalize (COS (rho_ub V * MaxT) H4 H5); intro; elim H6; intros; assumption. split. left; apply Rlt_le_trans with 0%R. replace (- PI / 2)%R with (- (PI / 2))%R. apply _PI2_RLT_0. unfold Rdiv in |- *; symmetry in |- *; apply Ropp_mult_distr_l_reverse. apply Rmult_le_pos. left; apply rho_ub_pos. left; unfold MaxT in |- *. prove_sup. cut (MaxT <= MaxT)%R. intro; left; apply (rho_ub_t_PI2 V (mkTimeT MaxT MinT_MaxT H3)). right; reflexivity. apply cos_decr_1. left; apply Rmult_lt_0_compat. apply rho_V_is_pos. apply Rlt_le_trans with MinT. apply MinT_is_pos. apply (cond_1 T). left; apply Rlt_trans with (PI / 2)%R. apply (rho_t_PI2 T). apply PI2_Rlt_PI. left; apply Rmult_lt_0_compat. apply rho_ub_pos. unfold MaxT in |- *; prove_sup. left; apply Rlt_trans with (PI / 2)%R. cut (MaxT <= MaxT)%R. intro; apply (rho_ub_t_PI2 V (mkTimeT MaxT MinT_MaxT H3)). right; reflexivity. apply PI2_Rlt_PI. apply Rmult_le_compat. left; apply rho_V_is_pos. left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]. left; unfold rho_V in |- *; apply rho_ub_0. apply (cond_2 T). ring. ring. Qed.
imports: Reals trajectory_const rrho constants Omega