proposition: Lemma Math_prop_approx_x_a_PI2 : forall (a l1 l2 : R) (T : TimeT), (0 <= a)%R -> (a <= PI / 2)%R -> (0 <= l1)%R -> (l1 <= l2)%R -> (r_lb V * sin_lb (rho_lb V * MinT) - l2 * cos_ub a <= r_V * sin (rho_V * T) - l1 * cos a)%R.
proof: Proof. intros; unfold Rminus in |- *; apply Rplus_le_compat. apply Rmult_le_compat. left; unfold r_lb in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply TypeSpeed_pos | apply Rinv_0_lt_compat; apply rho_ub_pos ]. apply sin_lb_ge_0. left; apply Rmult_lt_0_compat; [ apply rho_lb_pos | apply MinT_is_pos ]. apply Rle_trans with (rho_V * MinT)%R. apply Rmult_le_compat_r. left; apply MinT_is_pos. unfold rho_V in |- *; left; apply rho_lb_0. cut (MinT <= MinT)%R. intro; left; apply (rho_t_PI2 (mkTimeT MinT H3 MinT_MaxT)). right; reflexivity. unfold r_V in |- *; left; apply r_lb_0. apply Rle_trans with (sin (rho_lb V * MinT)). cut (0 <= rho_lb V * MinT <= PI)%R. intro; elim H3; intros. generalize (SIN (rho_lb V * MinT) H4 H5); intro; elim H6; intros; assumption. split. left; apply Rmult_lt_0_compat. apply rho_lb_pos. apply MinT_is_pos. left; apply Rle_lt_trans with (PI / 2)%R. apply Rle_trans with (rho_V * MinT)%R. apply Rmult_le_compat_r. left; apply MinT_is_pos. unfold rho_V in |- *; left; apply rho_lb_0. cut (MinT <= MinT)%R. intro; left; apply (rho_t_PI2 (mkTimeT MinT H3 MinT_MaxT)). right; reflexivity. apply PI2_Rlt_PI. apply sin_incr_1. left; apply Rlt_trans with 0%R. apply _PI2_RLT_0. apply Rmult_lt_0_compat. apply rho_lb_pos. apply MinT_is_pos. apply Rle_trans with (rho_V * MinT)%R. apply Rmult_le_compat_r. left; apply MinT_is_pos. unfold rho_V in |- *; left; apply rho_lb_0. cut (MinT <= MinT)%R. intro; left; apply (rho_t_PI2 (mkTimeT MinT H3 MinT_MaxT)). right; reflexivity. left; apply Rlt_trans with 0%R. apply _PI2_RLT_0. 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 (rho_t_PI2 T). apply Rmult_le_compat. left; apply rho_lb_pos. left; apply MinT_is_pos. left; unfold rho_V in |- *; apply rho_lb_0. apply (cond_1 T). apply Ropp_ge_le_contravar; apply Rle_ge. apply Rmult_le_compat. assumption. apply cos_ge_0. left; apply Rlt_le_trans with 0%R. apply _PI2_RLT_0. assumption. assumption. assumption. cut (- PI / 2 <= a)%R. intro; generalize (COS a H3 H0); intro; elim H4; intros; assumption. 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. assumption. Qed.
imports: Reals trajectory_const rrho constants Omega