proposition: Lemma m_rho_ub_0 : forall t : TimeT, (m_rho_ub t <= m t)%R.
proof: Proof. Proof with trivial. intro; unfold m_rho_ub, m in |- *; repeat rewrite Rmult_assoc; apply Rmult_le_compat_l... left; simpl in |- *; prove_sup0... cut (0 <= r_lb V <= r_V)%R... cut (0 <= sin_lb (rho_lb V * (t / 2)) <= sin (rho_V * (t / 2)))%R... intros; elim H; intros H1 H2; elim H0; intros H3 H4... apply Rmult_le_compat... cut (0 < rho_lb V * (t / 2) <= rho_V * (t / 2))%R... cut (rho_V * (t / 2) <= PI / 2)%R... intros; elim H0; intros H1 H2; split... left; apply sin_lb_gt_0... apply Rle_trans with (rho_V * (t / 2))%R... apply Rle_trans with (sin (rho_lb V * (t / 2)))... generalize (SIN (rho_lb V * (t / 2)) (Rlt_le 0 (rho_lb V * (t / 2)) H1) (Rle_trans (rho_lb V * (t / 2)) (PI / 2) PI (Rle_trans (rho_lb V * (t / 2)) (rho_V * (t / 2)) (PI / 2) H2 H) (Rlt_le (PI / 2) PI PI2_Rlt_PI)))... intro H3; elim H3; intros H4 H5... apply sin_incr_1... left; apply (Rlt_trans (- (PI / 2)) 0 (rho_lb V * (t / 2)) _PI2_RLT_0 H1)... apply Rle_trans with (rho_V * (t / 2))%R... left; apply (Rlt_trans (- (PI / 2)) 0 (rho_V * (t / 2)) _PI2_RLT_0 (Rlt_le_trans 0 (rho_lb V * (t / 2)) (rho_V * (t / 2)) H1 H2))... left; apply Rlt_trans with (PI / 4)%R... generalize (rho_t_PI2 t); intro H; unfold Rdiv in |- *; replace (/ 4)%R with (/ 2 * / 2)%R... repeat rewrite <- Rmult_assoc; apply Rmult_lt_compat_r... apply Rinv_0_lt_compat; prove_sup0... rewrite <- Rinv_mult_distr... discrR... discrR... apply PI4_RLT_PI2... split... unfold Rdiv in |- *; repeat simple apply Rmult_lt_0_compat... apply rho_lb_pos... apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 t)... apply Rinv_0_lt_compat; prove_sup0... apply Rmult_le_compat_r... left; unfold Rdiv in |- *; apply Rmult_lt_0_compat... apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 t)... apply Rinv_0_lt_compat; prove_sup0... unfold rho_V in |- *... left; apply rho_lb_0... split... unfold r_lb in |- *... unfold Rdiv in |- *; left; apply Rmult_lt_0_compat... apply (TypeSpeed_pos V)... apply Rinv_0_lt_compat; apply rho_ub_pos... unfold r_V in |- *; left; apply r_lb_0... Qed.
imports: Reals trajectory_const rrho trajectory_def